--- a/src/Pure/pure_thy.ML Mon Feb 15 17:17:51 2010 +0100
+++ b/src/Pure/pure_thy.ML Mon Feb 15 18:03:42 2010 +0100
@@ -313,7 +313,7 @@
(Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
("Pure.term", typ "logic => prop", Delimfix "TERM _"),
- ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&&", 2))]
+ ("Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
@@ -325,9 +325,9 @@
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", typ "'a", NoSyn),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- ("==", typ "'a => 'a => prop", InfixrName ("\\<equiv>", 2)),
+ ("==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- ("==>", typ "prop => prop => prop", InfixrName ("\\<Longrightarrow>", 1)),
+ ("==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
@@ -336,7 +336,7 @@
#> Sign.add_modesyntax_i ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts_i
- [(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)),
+ [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
(Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
(Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
(Binding.name "prop", typ "prop => prop", NoSyn),