--- a/src/Pure/Isar/isar_syn.ML Tue Feb 26 21:44:29 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Feb 26 21:44:48 2002 +0100
@@ -295,15 +295,15 @@
(* statements *)
val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
-val long_statement =
+val general_statement =
statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
fun gen_theorem k =
OuterSyntax.command k ("state " ^ k) K.thy_goal
- (Scan.optional (P.thm_name ":" --|
- Scan.ahead (P.$$$ "(" || P.locale_keyword || P.$$$ "shows")) ("", [])
- -- P.locale_target -- long_statement >> (fn ((x, y), (z, w)) =>
- (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x (y, z) w))));
+ (P.locale_target -- Scan.optional (P.thm_name ":" --|
+ Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
+ general_statement >> (fn ((x, y), (z, w)) =>
+ (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x y z w))));
val theoremP = gen_theorem Drule.theoremK;
val lemmaP = gen_theorem Drule.lemmaK;
@@ -717,11 +717,10 @@
val keywords =
["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
"<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
- "concl", "defines", "files", "fixes", "in", "infix", "infixl",
- "infixr", "is", "notes", "output", "overloaded", "shows",
- "structure", "uses", "where", "|", "\\<equiv>",
- "\\<leftharpoondown>", "\\<rightharpoonup>",
- "\\<rightleftharpoons>", "\\<subseteq>"];
+ "concl", "defines", "files", "fixes", "in", "includes", "infix",
+ "infixl", "infixr", "is", "notes", "output", "overloaded", "shows",
+ "structure", "where", "|", "\\<equiv>", "\\<leftharpoondown>",
+ "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"];
val parsers = [
(*theory structure*)