'defs': unchecked flag;
authorwenzelm
Sat May 13 02:51:43 2006 +0200 (2006-05-13 ago)
changeset 196314445b353f78b
parent 19630 d370c3f5d3b2
child 19632 21e04f0edd82
'defs': unchecked flag;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:42 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:43 2006 +0200
     1.3 @@ -181,9 +181,15 @@
     1.4    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     1.5      (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
     1.6  
     1.7 +val opt_unchecked_overloaded =
     1.8 +  Scan.optional (P.$$$ "(" |-- P.!!!
     1.9 +    (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
    1.10 +      P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
    1.11 +
    1.12  val defsP =
    1.13    OuterSyntax.command "defs" "define constants" K.thy_decl
    1.14 -    (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
    1.15 +    (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
    1.16 +      >> (Toplevel.theory o IsarThy.add_defs));
    1.17  
    1.18  
    1.19  (* constant definitions and abbreviations *)
    1.20 @@ -870,7 +876,7 @@
    1.21    "begin", "binder", "concl", "constrains", "defines", "fixes",
    1.22    "imports", "in", "includes", "infix", "infixl", "infixr", "is",
    1.23    "notes", "obtains", "open", "output", "overloaded", "shows",
    1.24 -  "structure", "uses", "where", "|", "\\<equiv>",
    1.25 +  "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
    1.26    "\\<leftharpoondown>", "\\<rightharpoonup>",
    1.27    "\\<rightleftharpoons>", "\\<subseteq>"];
    1.28