src/Pure/sign.ML
changeset 2211 0487add593b5
parent 2197 e895937fcd56
child 2228 f381c1a98209
     1.1 --- a/src/Pure/sign.ML	Tue Nov 19 13:21:28 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Nov 19 14:20:02 1996 +0100
     1.3 @@ -616,9 +616,11 @@
     1.4    |> add_consts
     1.5     [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
     1.6      ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     1.7 -    ("==>", "[prop, prop] => prop", InfixrName ("==>", 1)),
     1.8 +    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     1.9      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.10      ("TYPE", "'a itself", NoSyn)]
    1.11 +  |> add_syntax
    1.12 +   [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
    1.13    |> add_name "ProtoPure";
    1.14  
    1.15  val pure = proto_pure