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