# HG changeset patch # User wenzelm # Date 1563716563 -7200 # Node ID 2adff54de67eb4adf58652b6d5dad5010d6ca610 # Parent e31271559de844c454d3e49b9693980696a8d0ce discontinued ASCII syntax; diff -r e31271559de8 -r 2adff54de67e src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sun Jul 21 15:19:07 2019 +0200 +++ b/src/Doc/Implementation/Logic.thy Sun Jul 21 15:42:43 2019 +0200 @@ -1147,11 +1147,8 @@ \begin{center} \begin{supertabular}{rclr} - @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\ - & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\ - & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\ + @{syntax_def (inner) proof} & = & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\ & \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\ - & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\ & \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\ & \<open>|\<close> & \<open>id | longid\<close> \\ \\ diff -r e31271559de8 -r 2adff54de67e src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Jul 21 15:19:07 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Jul 21 15:42:43 2019 +0200 @@ -53,10 +53,6 @@ (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")] - |> Sign.add_syntax (Print_Mode.ASCII, true) - [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)), - (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), - (Lexicon.mark_const "Pure.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")