'defs': unchecked flag;
authorwenzelm
Sat, 13 May 2006 02:51:43 +0200 (2006-05-13)
changeset 19631 4445b353f78b
parent 19630 d370c3f5d3b2
child 19632 21e04f0edd82
'defs': unchecked flag;
src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:42 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:43 2006 +0200
@@ -181,9 +181,15 @@
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
 
+val opt_unchecked_overloaded =
+  Scan.optional (P.$$$ "(" |-- P.!!!
+    (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
+      P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
+
 val defsP =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
+    (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
+      >> (Toplevel.theory o IsarThy.add_defs));
 
 
 (* constant definitions and abbreviations *)
@@ -870,7 +876,7 @@
   "begin", "binder", "concl", "constrains", "defines", "fixes",
   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   "notes", "obtains", "open", "output", "overloaded", "shows",
-  "structure", "uses", "where", "|", "\\<equiv>",
+  "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",
   "\\<rightleftharpoons>", "\\<subseteq>"];