equal
deleted
inserted
replaced
74 in |
74 in |
75 thy |
75 thy |
76 end; |
76 end; |
77 |
77 |
78 (** outer syntax **) |
78 (** outer syntax **) |
79 |
|
80 local structure P = Parse and K = Keyword in |
|
81 |
|
82 val _ = |
79 val _ = |
83 Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl |
80 Outer_Syntax.command ("atom_decl", Keyword.thy_decl) |
84 ((P.binding -- Scan.option (Args.parens (P.binding))) >> |
81 "declaration of a concrete atom type" |
85 (Toplevel.print oo (Toplevel.theory o add_atom_decl))); |
82 ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >> |
|
83 (Toplevel.print oo (Toplevel.theory o add_atom_decl))) |
86 |
84 |
87 end; |
85 end; |
88 |
|
89 end; |
|