equal
deleted
inserted
replaced
179 |
179 |
180 (* axioms and definitions *) |
180 (* axioms and definitions *) |
181 |
181 |
182 val _ = |
182 val _ = |
183 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl |
183 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl |
184 (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms)); |
184 (Scan.repeat1 SpecParse.spec >> |
|
185 (Toplevel.theory o |
|
186 (IsarCmd.add_axioms o |
|
187 tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead")))); |
185 |
188 |
186 val opt_unchecked_overloaded = |
189 val opt_unchecked_overloaded = |
187 Scan.optional (P.$$$ "(" |-- P.!!! |
190 Scan.optional (P.$$$ "(" |-- P.!!! |
188 (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false || |
191 (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false || |
189 P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false); |
192 P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false); |