Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_syntax.ML
changeset 56206 7adec2a527f5
parent 56161 300f613060b0
child 56239 17df7145a871 
--- a/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:16:28 2014 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Mar 18 16:44:51 2014 +0100
@@ -63,9 +63,9 @@
        ("", idtT --> paramsT, Delimfix "_"),
        ("", paramT --> paramsT, Delimfix "_")]
   |> Sign.add_modesyntax_i (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))]
+      [("_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_trrules (map Syntax.Parse_Print_Rule
       [(Ast.mk_appl (Ast.Constant "_Lam")
           [Ast.mk_appl (Ast.Constant "_Lam0")
isabelle