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, Trindemossen-1