--- a/src/Pure/pure_thy.ML Sun Mar 06 13:19:19 2016 +0100
+++ b/src/Pure/pure_thy.ML Sun Mar 06 16:19:02 2016 +0100
@@ -108,12 +108,12 @@
("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
("", typ "type => types", Delimfix "_"),
("_types", typ "type => types => types", Delimfix "_,/ _"),
- ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+ ("\<^type>fun", typ "type => type => type", Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
("", typ "type => type", Delimfix "'(_')"),
- ("\\<^type>dummy", typ "type", Delimfix "'_"),
+ ("\<^type>dummy", typ "type", Delimfix "'_"),
("_type_prop", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
("_abs", typ "'a", NoSyn),
("", typ "'a => args", Delimfix "_"),
("_args", typ "'a => args => args", Delimfix "_,/ _"),
@@ -131,26 +131,26 @@
("", typ "id_position => aprop", Delimfix "_"),
("", typ "longid_position => aprop", Delimfix "_"),
("", typ "var_position => aprop", Delimfix "_"),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_DDDOT", typ "aprop", Delimfix "\<dots>"),
("_aprop", typ "aprop => prop", Delimfix "PROP _"),
("_asm", typ "prop => asms", Delimfix "_"),
("_asms", typ "prop => asms => asms", Delimfix "_;/ _"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_mk_ofclass", typ "dummy", NoSyn),
("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
("", typ "id_position => logic", Delimfix "_"),
("", typ "longid_position => logic", Delimfix "_"),
("", typ "var_position => logic", Delimfix "_"),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>"),
+ ("_DDDOT", typ "logic", Delimfix "\<dots>"),
("_strip_positions", typ "'a", NoSyn),
("_position", typ "num_token => num_position", Delimfix "_"),
("_position", typ "float_token => float_position", Delimfix "_"),
("_constify", typ "num_position => num_const", Delimfix "_"),
("_constify", typ "float_position => float_const", Delimfix "_"),
- ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
+ ("_index", typ "logic => index", Delimfix "(00\<^bsub>_\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
- ("_indexvar", typ "index", Delimfix "'\\<index>"),
+ ("_indexvar", typ "index", Delimfix "'\<index>"),
("_struct", typ "index => logic", NoSyn),
("_update_name", typ "idt", NoSyn),
("_constrainAbs", typ "'a", NoSyn),
@@ -189,9 +189,9 @@
#> Sign.add_syntax ("", false)
[(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_consts
- [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
- (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\<And>", 0, 0)),
+ [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
+ (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
+ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
(qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
(qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
(qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]