added 'if' and 'for' keywords;
authorwenzelm
Wed Jun 07 02:01:32 2006 +0200 (2006-06-07)
changeset 19809b8f35de1c664
parent 19808 396dd23c54ef
child 19810 dae765e552ce
added 'if' and 'for' keywords;
tuned;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jun 07 02:01:31 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 07 02:01:32 2006 +0200
     1.3 @@ -356,22 +356,19 @@
     1.4        >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) =>
     1.5               Locale.add_locale is_open name expr elems #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
     1.6  
     1.7 -val opt_inst =
     1.8 -  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
     1.9 -
    1.10  val interpretationP =
    1.11    OuterSyntax.command "interpretation"
    1.12      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    1.13      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr
    1.14        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale)) ||
    1.15 -     P.opt_thm_name ":" -- P.locale_expr -- opt_inst >> (fn ((x, y), z) =>
    1.16 +     P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
    1.17        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation x y z)));
    1.18  
    1.19  val interpretP =
    1.20    OuterSyntax.command "interpret"
    1.21      "prove and register interpretation of locale expression in proof context"
    1.22      (K.tag_proof K.prf_goal)
    1.23 -    (P.opt_thm_name ":" -- P.locale_expr -- opt_inst >> (fn ((x, y), z) =>
    1.24 +    (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
    1.25        Toplevel.print o Toplevel.proof' (Locale.interpret x y z)));
    1.26  
    1.27  
    1.28 @@ -879,9 +876,9 @@
    1.29  val _ = OuterSyntax.add_keywords
    1.30   ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.31    "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
    1.32 -  "begin", "binder", "concl", "constrains", "defines", "fixes",
    1.33 -  "imports", "in", "includes", "infix", "infixl", "infixr", "is",
    1.34 -  "notes", "obtains", "open", "output", "overloaded", "shows",
    1.35 +  "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
    1.36 +  "imports", "if", "in", "includes", "infix", "infixl", "infixr",
    1.37 +  "is", "notes", "obtains", "open", "output", "overloaded", "shows",
    1.38    "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
    1.39    "\\<leftharpoondown>", "\\<rightharpoonup>",
    1.40    "\\<rightleftharpoons>", "\\<subseteq>"];