src/Pure/sign.ML
changeset 2095 e8544d73a7aa
parent 1890 a525e960f2bd
child 2138 056dead45ae8
equal deleted inserted replaced
2094:2061df98aab5 2095:e8544d73a7aa
   577   |> add_syntax Syntax.pure_syntax
   577   |> add_syntax Syntax.pure_syntax
   578   |> add_trfuns Syntax.pure_trfuns
   578   |> add_trfuns Syntax.pure_trfuns
   579   |> add_consts
   579   |> add_consts
   580    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   580    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   581     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   581     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   582     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
   582     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   583     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   583     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   584     ("TYPE", "'a itself", NoSyn)]
   584     ("TYPE", "'a itself", NoSyn)]
   585   |> add_name "ProtoPure";
   585   |> add_name "ProtoPure";
   586 
   586 
   587 val pure = proto_pure
   587 val pure = proto_pure