src/Pure/pure_thy.ML
changeset 56245 84fc7dfa3cd4
parent 56244 3298b7a2795a
child 56436 30ccec1e82fb
     1.1 --- a/src/Pure/pure_thy.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4      ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
     1.5      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     1.6      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     1.7 -    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     1.8 +    (const "Pure.imp",  typ "prop => prop => prop",     Delimfix "op ==>"),
     1.9      (const "Pure.dummy_pattern", typ "aprop",          Delimfix "'_"),
    1.10      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    1.11      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    1.12 @@ -184,9 +184,9 @@
    1.13      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    1.14      ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    1.15      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    1.16 -    (const "==",          typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
    1.17 -    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    1.18 -    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    1.19 +    (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
    1.20 +    (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    1.21 +    (const "Pure.imp",    typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    1.22      ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
    1.23      ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    1.24      ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
    1.25 @@ -195,15 +195,15 @@
    1.26    #> Sign.add_syntax ("HTML", false)
    1.27     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    1.28    #> Sign.add_consts
    1.29 -   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
    1.30 -    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    1.31 -    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.32 +   [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
    1.33 +    (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    1.34 +    (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.35      (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
    1.36      (qualify (Binding.name "type"), typ "'a itself", NoSyn),
    1.37      (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
    1.38 -  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
    1.39 -  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
    1.40 -  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
    1.41 +  #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
    1.42 +  #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
    1.43 +  #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
    1.44    #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
    1.45    #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
    1.46    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation