src/Pure/Isar/outer_parse.ML
changeset 16169 b59202511b8a
parent 16102 c5f6726d9bb1
child 16498 9d265401fee0
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Jun 01 12:30:49 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Jun 01 12:30:50 2005 +0200
     1.3 @@ -314,11 +314,14 @@
     1.4  local
     1.5  
     1.6  val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME;
     1.7 -val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
     1.8 +val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||
     1.9 +   $$$ "defines" || $$$ "notes" || $$$ "includes";
    1.10  
    1.11  val loc_element =
    1.12    $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
    1.13      >> triple1)) >> Locale.Fixes ||
    1.14 +  $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
    1.15 +    >> Locale.Constrains ||
    1.16    $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
    1.17      >> Locale.Assumes ||
    1.18    $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))