Structure emitOrdinalTheory

Source File	Identifier index	Theory binding index

signature emitOrdinalTheory =
sig
  type thm = Thm.thm
(*
   [basis_emit] Parent theory of "emitOrdinal"
   
   [ordinalNotation] Parent theory of "emitOrdinal"
   
   
*)
end

Source File	Identifier index	Theory binding index

HOL 4, Trindemossen-2