equal
deleted
inserted
replaced
69 thy |
69 thy |
70 end; |
70 end; |
71 |
71 |
72 (** outer syntax **) |
72 (** outer syntax **) |
73 |
73 |
74 local structure P = OuterParse and K = OuterKeyword in |
74 local structure P = Parse and K = Keyword in |
75 |
75 |
76 val _ = |
76 val _ = |
77 OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl |
77 Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl |
78 ((P.binding -- Scan.option (Args.parens (P.binding))) >> |
78 ((P.binding -- Scan.option (Args.parens (P.binding))) >> |
79 (Toplevel.print oo (Toplevel.theory o add_atom_decl))); |
79 (Toplevel.print oo (Toplevel.theory o add_atom_decl))); |
80 |
80 |
81 end; |
81 end; |
82 |
82 |