src/Pure/pure_thy.ML
changeset 42294 0f4372a2d2e4
parent 42293 6cca0343ea48
child 42295 8fdbb3b10beb
     1.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 17:45:37 2011 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 18:08:13 2011 +0200
     1.3 @@ -61,8 +61,16 @@
     1.4      (Binding.name "itself", 1, NoSyn),
     1.5      (Binding.name "dummy", 0, NoSyn)]
     1.6    #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
     1.7 +  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
     1.8    #> Sign.add_syntax_i
     1.9 -   [("",            typ "tid => type",                 Delimfix "_"),
    1.10 +   [("",            typ "prop' => prop",               Delimfix "_"),
    1.11 +    ("",            typ "logic => any",                Delimfix "_"),
    1.12 +    ("",            typ "prop' => any",                Delimfix "_"),
    1.13 +    ("",            typ "logic => logic",              Delimfix "'(_')"),
    1.14 +    ("",            typ "prop' => prop'",              Delimfix "'(_')"),
    1.15 +    ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
    1.16 +    ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
    1.17 +    ("",            typ "tid => type",                 Delimfix "_"),
    1.18      ("",            typ "tvar => type",                Delimfix "_"),
    1.19      ("",            typ "type_name => type",           Delimfix "_"),
    1.20      ("_type_name",  typ "id => type_name",             Delimfix "_"),