--- a/src/Pure/Proof/proof_syntax.ML Mon Dec 28 23:13:33 2015 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Tue Dec 29 14:58:15 2015 +0100
@@ -46,8 +46,8 @@
|> Sign.add_types_global
[(Binding.make ("proof", @{here}), 0, NoSyn)]
|> fold (snd oo Sign.declare_const_global)
- [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
- ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+ [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
@@ -58,17 +58,17 @@
[Binding.make ("param", @{here}),
Binding.make ("params", @{here})]
|> Sign.add_syntax Syntax.mode_default
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
("", paramT --> paramT, Delimfix "'(_')"),
("", idtT --> paramsT, Delimfix "_"),
("", paramT --> paramsT, Delimfix "_")]
- |> Sign.add_syntax (Symbol.xsymbolsN, true)
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
+ |> Sign.add_syntax (Print_Mode.ASCII, true)
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
[(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam0")
--- a/src/Pure/pure_thy.ML Mon Dec 28 23:13:33 2015 +0100
+++ b/src/Pure/pure_thy.ML Tue Dec 29 14:58:15 2015 +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 ("(_/ => _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [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_prop", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [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,18 +131,18 @@
("", typ "id_position => aprop", Delimfix "_"),
("", typ "longid_position => aprop", Delimfix "_"),
("", typ "var_position => aprop", Delimfix "_"),
- ("_DDDOT", typ "aprop", Delimfix "..."),
+ ("_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 ("((3[| _ |])/ ==> _)", [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 "..."),
+ ("_DDDOT", typ "logic", Delimfix "\\<dots>"),
("_strip_positions", typ "'a", NoSyn),
("_position", typ "num_token => num_position", Delimfix "_"),
("_position", typ "float_token => float_position", Delimfix "_"),
@@ -171,30 +171,27 @@
("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
- (const "Pure.imp", typ "prop => prop => prop", Delimfix "op ==>"),
(const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax Syntax.mode_default applC_syntax
- #> Sign.add_syntax (Symbol.xsymbolsN, true)
- [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
- (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "Pure.imp", 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>")]
+ #> Sign.add_syntax (Print_Mode.ASCII, true)
+ [(tycon "fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
+ (const "Pure.eq", typ "'a => 'a => prop", Infix ("==", 2)),
+ (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
+ (const "Pure.imp", typ "prop => prop => prop", Infixr ("==>", 1)),
+ ("_DDDOT", typ "aprop", Delimfix "..."),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", Delimfix "...")]
#> Sign.add_syntax ("", false)
[(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
- #> Sign.add_syntax ("HTML", false)
- [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
- [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)),
- (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
- (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 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 "'_")]