Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/outer_parse.ML
changeset 16169 b59202511b8a
parent 16102 c5f6726d9bb1
child 16498 9d265401fee0 
--- a/src/Pure/Isar/outer_parse.ML	Wed Jun 01 12:30:49 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Jun 01 12:30:50 2005 +0200
@@ -314,11 +314,14 @@
 local
 
 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME;
-val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
+val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||
+   $$$ "defines" || $$$ "notes" || $$$ "includes";
 
 val loc_element =
   $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
     >> triple1)) >> Locale.Fixes ||
+  $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
+    >> Locale.Constrains ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
     >> Locale.Assumes ||
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
isabelle