restored changed prettyprinting of ==>;
authorwenzelm
Tue Nov 19 14:20:02 1996 +0100 (1996-11-19)
changeset 22110487add593b5
parent 2210 8369f3f4bb4f
child 2212 bd705e9de196
restored changed prettyprinting of ==>;
src/Pure/sign.ML
     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