discontinued ASCII syntax;
authorwenzelm
Sun Jul 21 15:42:43 2019 +0200 (4 weeks ago)
changeset 703892adff54de67e
parent 70388 e31271559de8
child 70390 772321761cb8
discontinued ASCII syntax;
src/Doc/Implementation/Logic.thy
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/Doc/Implementation/Logic.thy	Sun Jul 21 15:19:07 2019 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Jul 21 15:42:43 2019 +0200
     1.3 @@ -1147,11 +1147,8 @@
     1.4    \begin{center}
     1.5    \begin{supertabular}{rclr}
     1.6  
     1.7 -  @{syntax_def (inner) proof} & = & \<^verbatim>\<open>Lam\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
     1.8 -    & \<open>|\<close> & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
     1.9 -    & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%\<close> \<open>any\<close> \\
    1.10 +  @{syntax_def (inner) proof} & = & \<open>\<^bold>\<lambda>\<close> \<open>params\<close> \<^verbatim>\<open>.\<close> \<open>proof\<close> \\
    1.11      & \<open>|\<close> & \<open>proof\<close> \<open>\<cdot>\<close> \<open>any\<close> \\
    1.12 -    & \<open>|\<close> & \<open>proof\<close> \<^verbatim>\<open>%%\<close> \<open>proof\<close> \\
    1.13      & \<open>|\<close> & \<open>proof\<close> \<open>\<bullet>\<close> \<open>proof\<close> \\
    1.14      & \<open>|\<close> & \<open>id  |  longid\<close> \\
    1.15    \\
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:19:07 2019 +0200
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:42:43 2019 +0200
     2.3 @@ -53,10 +53,6 @@
     2.4       (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
     2.5       (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
     2.6       (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")]
     2.7 -  |> Sign.add_syntax (Print_Mode.ASCII, true)
     2.8 -    [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
     2.9 -     (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
    2.10 -     (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
    2.11    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
    2.12      [(Ast.mk_appl (Ast.Constant "_Lam")
    2.13          [Ast.mk_appl (Ast.Constant "_Lam0")