Structure emitOrdinalTheory

Source File	Identifier index	Theory binding index

signature emitOrdinalTheory =
sig
  type thm = Thm.thm
  
  val emitOrdinal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [basis_emit] Parent theory of "emitOrdinal"
   
   [ordinalNotation] Parent theory of "emitOrdinal"
   
   
*)
end

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-14