Theory Enum_Type

section ‹ Enumeration Types ›

theory Enum_Type
  imports Haskell_Show
  keywords "enumtype" :: "thy_defn"
begin

ML_file ‹Enum_Type.ML›

ML ‹ 
val _ =
  Outer_Syntax.command @{command_keyword enumtype} "define enumeration types"
   ((Parse.name -- (@{keyword "="} |-- Scan.repeat (Parse.name --| @{keyword "|"}) -- Parse.name)) >> (fn (tname, (cs, c)) => Toplevel.theory (Enum_Type.enum_type tname (cs @ [c]))));
›

declare UNIV_enum [code_unfold]

end