--- a/src/Pure/sign.ML Tue Nov 19 13:21:28 1996 +0100
+++ b/src/Pure/sign.ML Tue Nov 19 14:20:02 1996 +0100
@@ -616,9 +616,11 @@
|> add_consts
[("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
- ("==>", "[prop, prop] => prop", InfixrName ("==>", 1)),
+ ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
("TYPE", "'a itself", NoSyn)]
+ |> add_syntax
+ [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
|> add_name "ProtoPure";
val pure = proto_pure