equal
deleted
inserted
replaced
75 thy |
75 thy |
76 end; |
76 end; |
77 |
77 |
78 (** outer syntax **) |
78 (** outer syntax **) |
79 val _ = |
79 val _ = |
80 Outer_Syntax.command ("atom_decl", Keyword.thy_decl) |
80 Outer_Syntax.command @{command_spec "atom_decl"} |
81 "declaration of a concrete atom type" |
81 "declaration of a concrete atom type" |
82 ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> |
82 ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> |
83 (Toplevel.print oo (Toplevel.theory o add_atom_decl))) |
83 (Toplevel.print oo (Toplevel.theory o add_atom_decl))) |
84 |
84 |
85 end; |
85 end; |