Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned long_statement;
authorwenzelm
Tue, 26 Feb 2002 18:20:01 +0100
changeset 12952 2d6156232994
parent 12951 a9fdcb71d252
child 12953 7d5bd53555d8
tuned long_statement;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 26 15:45:32 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 26 18:20:01 2002 +0100
@@ -296,7 +296,7 @@
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
 val long_statement =
-  Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement) || statement >> pair [];
+  statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal
isabelle