src/Pure/sign.ML
changeset 2211 0487add593b5
parent 2197 e895937fcd56
child 2228 f381c1a98209
equal deleted inserted replaced
2210:8369f3f4bb4f 2211:0487add593b5
   614   |> add_modesyntax ("symbolfont", Syntax.pure_symfont_syntax)
   614   |> add_modesyntax ("symbolfont", Syntax.pure_symfont_syntax)
   615   |> add_trfuns Syntax.pure_trfuns
   615   |> add_trfuns Syntax.pure_trfuns
   616   |> add_consts
   616   |> add_consts
   617    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   617    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   618     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   618     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   619     ("==>", "[prop, prop] => prop", InfixrName ("==>", 1)),
   619     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   620     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   620     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   621     ("TYPE", "'a itself", NoSyn)]
   621     ("TYPE", "'a itself", NoSyn)]
       
   622   |> add_syntax
       
   623    [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   622   |> add_name "ProtoPure";
   624   |> add_name "ProtoPure";
   623 
   625 
   624 val pure = proto_pure
   626 val pure = proto_pure
   625   |> add_syntax Syntax.pure_appl_syntax
   627   |> add_syntax Syntax.pure_appl_syntax
   626   |> add_name "Pure";
   628   |> add_name "Pure";