src/Pure/pure_thy.ML
changeset 61143 5f898411ce87
parent 58421 37cbbd8eb460
child 61246 077b88f9ec16
     1.1 --- a/src/Pure/pure_thy.ML	Wed Sep 09 11:24:34 2015 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Sep 09 14:47:41 2015 +0200
     1.3 @@ -176,11 +176,6 @@
     1.4    #> Sign.add_syntax (Symbol.xsymbolsN, true)
     1.5     [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
     1.6      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
     1.7 -    ("_ofsort",           typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
     1.8 -    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
     1.9 -    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    1.10 -    ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    1.11 -    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    1.12      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    1.13      (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
    1.14      (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),