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.
group locale_element;
authorwenzelm
Tue, 06 Nov 2001 01:19:07 +0100
changeset 12064 34c270893ecb
parent 12063 4c16bdee47d4
child 12065 5f7f44d5e3dd
group locale_element;
src/Pure/Isar/outer_parse.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/outer_parse.ML	Tue Nov 06 01:18:46 2001 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 06 01:19:07 2001 +0100
@@ -305,15 +305,15 @@
 
 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
 
-val locale_element =
-  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix >> triple1))
-    >> Locale.Fixes ||
+val locale_element = group "locale element"
+  ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
+    >> triple1)) >> Locale.Fixes ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
     >> Locale.Assumes ||
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
     >> Locale.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
-  $$$ "uses" |-- (!!! ($$$ "FIXME" >> K ())) >> Locale.Uses;
+  $$$ "uses" |-- (!!! ($$$ "FIXME" >> K ())) >> Locale.Uses);
 
 
 (* proof methods *)
isabelle