prefer Input.source (via cartouche);
authorwenzelm
Mon Nov 27 10:21:52 2017 +0100 (16 months ago)
changeset 67093835a2ab92c3d
parent 67092 d7b3876d3ab1
child 67094 4a2563645635
prefer Input.source (via cartouche);
src/HOL/Tools/rewrite_hol_proof.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 27 10:04:17 2017 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 27 10:21:52 2017 +0100
     1.3 @@ -13,293 +13,294 @@
     1.4  structure RewriteHOLProof : REWRITE_HOL_PROOF =
     1.5  struct
     1.6  
     1.7 -val rews = map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o
     1.8 -    Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
     1.9 +val rews =
    1.10 +  map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o Logic.dest_equals o
    1.11 +    Logic.varify_global o Proof_Syntax.read_term @{theory} true propT o Syntax.implode_input)
    1.12  
    1.13    (** eliminate meta-equality rules **)
    1.14  
    1.15 -  ["(equal_elim % x1 % x2 %% \
    1.16 - \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
    1.17 - \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
    1.18 - \  (iffD1 % A % B %%  \
    1.19 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    1.20 +  [\<open>(equal_elim % x1 % x2 %%
    1.21 +      (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%
    1.22 +        (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==
    1.23 +    (iffD1 % A % B %%
    1.24 +      (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))\<close>,
    1.25  
    1.26 -   "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    1.27 - \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    1.28 - \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
    1.29 - \  (iffD2 % A % B %%  \
    1.30 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))",
    1.31 +   \<open>(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%
    1.32 +      (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%
    1.33 +        (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==
    1.34 +    (iffD2 % A % B %%
    1.35 +      (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))\<close>,
    1.36  
    1.37 -   "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%  \
    1.38 - \    (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==  \
    1.39 - \  (cong % TYPE('T) % TYPE('U) % f % g % x % y %%  \
    1.40 - \    (OfClass type_class % TYPE('T)) %% prfU %%  \
    1.41 - \    (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%  \
    1.42 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))",
    1.43 +   \<open>(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %%
    1.44 +      (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) ==
    1.45 +    (cong % TYPE('T) % TYPE('U) % f % g % x % y %%
    1.46 +      (OfClass type_class % TYPE('T)) %% prfU %%
    1.47 +      (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %%
    1.48 +      (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))\<close>,
    1.49  
    1.50 -   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%  \
    1.51 - \    (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==  \
    1.52 - \  (HOL.trans % TYPE('T) % x % y % z %% prfT %%  \
    1.53 - \    (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%  \
    1.54 - \    (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))",
    1.55 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %%
    1.56 +      (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) ==
    1.57 +    (HOL.trans % TYPE('T) % x % y % z %% prfT %%
    1.58 +      (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %%
    1.59 +      (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))\<close>,
    1.60  
    1.61 -   "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==  \
    1.62 - \  (HOL.refl % TYPE('T) % x %% prfT)",
    1.63 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) ==
    1.64 +    (HOL.refl % TYPE('T) % x %% prfT)\<close>,
    1.65  
    1.66 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    1.67 - \    (axm.symmetric % TYPE('T) % x % y %% prf)) ==  \
    1.68 - \  (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))",
    1.69 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%
    1.70 +      (axm.symmetric % TYPE('T) % x % y %% prf)) ==
    1.71 +    (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))\<close>,
    1.72  
    1.73 -   "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%  \
    1.74 - \    (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==  \
    1.75 - \  (ext % TYPE('T) % TYPE('U) % f % g %%  \
    1.76 - \    (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%  \
    1.77 - \    (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%  \
    1.78 - \       (OfClass type_class % TYPE('U)) %% (prf % x)))",
    1.79 +   \<open>(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %%
    1.80 +      (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) ==
    1.81 +    (ext % TYPE('T) % TYPE('U) % f % g %%
    1.82 +      (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %%
    1.83 +      (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %%
    1.84 +         (OfClass type_class % TYPE('U)) %% (prf % x)))\<close>,
    1.85  
    1.86 -   "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%  \
    1.87 - \    (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf",
    1.88 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %%
    1.89 +      (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf\<close>,
    1.90  
    1.91 -   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
    1.92 - \    (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
    1.93 - \      (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
    1.94 - \        (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==  \
    1.95 - \  (iffD1 % A = C % B = D %%  \
    1.96 - \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
    1.97 - \      prfT %% arity_type_bool %%  \
    1.98 - \      (cong % TYPE('T) % TYPE('T=>bool) %  \
    1.99 - \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
   1.100 - \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
   1.101 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
   1.102 - \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   1.103 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   1.104 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   1.105 - \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))",
   1.106 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%
   1.107 +      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%
   1.108 +        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%
   1.109 +          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) ==
   1.110 +    (iffD1 % A = C % B = D %%
   1.111 +      (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%
   1.112 +        prfT %% arity_type_bool %%
   1.113 +        (cong % TYPE('T) % TYPE('T=>bool) %
   1.114 +          (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%
   1.115 +          prfT %% (OfClass type_class % TYPE('T=>bool)) %%
   1.116 +          (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%
   1.117 +             (OfClass type_class % TYPE('T=>'T=>bool))) %%
   1.118 +          (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%
   1.119 +        (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%
   1.120 +      (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))\<close>,
   1.121  
   1.122 -   "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%  \
   1.123 - \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
   1.124 - \      (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%  \
   1.125 - \        (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%  \
   1.126 - \          (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==  \
   1.127 - \  (iffD2 % A = C % B = D %%  \
   1.128 - \    (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%  \
   1.129 - \      prfT %% arity_type_bool %%  \
   1.130 - \      (cong % TYPE('T) % TYPE('T=>bool) %  \
   1.131 - \        (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%  \
   1.132 - \        prfT %% (OfClass type_class % TYPE('T=>bool)) %%  \
   1.133 - \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%  \
   1.134 - \           (OfClass type_class % TYPE('T=>'T=>bool))) %%  \
   1.135 - \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%  \
   1.136 - \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%  \
   1.137 - \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))",
   1.138 +   \<open>(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %%
   1.139 +      (axm.symmetric % TYPE('T2) % x5 % x6 %%
   1.140 +        (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %%
   1.141 +          (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %%
   1.142 +            (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) ==
   1.143 +    (iffD2 % A = C % B = D %%
   1.144 +      (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %%
   1.145 +        prfT %% arity_type_bool %%
   1.146 +        (cong % TYPE('T) % TYPE('T=>bool) %
   1.147 +          (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %%
   1.148 +          prfT %% (OfClass type_class % TYPE('T=>bool)) %%
   1.149 +          (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %%
   1.150 +             (OfClass type_class % TYPE('T=>'T=>bool))) %%
   1.151 +          (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %%
   1.152 +        (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %%
   1.153 +      (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))\<close>,
   1.154  
   1.155     (** rewriting on bool: insert proper congruence rules for logical connectives **)
   1.156  
   1.157     (* All *)
   1.158  
   1.159 -   "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   1.160 - \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   1.161 - \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   1.162 - \  (allI % TYPE('a) % Q %% prfa %%  \
   1.163 - \    (Lam x.  \
   1.164 - \        iffD1 % P x % Q x %% (prf % x) %%  \
   1.165 - \         (spec % TYPE('a) % P % x %% prfa %% prf')))",
   1.166 +   \<open>(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%
   1.167 +      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.168 +      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.169 +    (allI % TYPE('a) % Q %% prfa %%
   1.170 +      (Lam x.
   1.171 +          iffD1 % P x % Q x %% (prf % x) %%
   1.172 +           (spec % TYPE('a) % P % x %% prfa %% prf')))\<close>,
   1.173  
   1.174 -   "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%  \
   1.175 - \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   1.176 - \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   1.177 - \  (allI % TYPE('a) % P %% prfa %%  \
   1.178 - \    (Lam x.  \
   1.179 - \        iffD2 % P x % Q x %% (prf % x) %%  \
   1.180 - \         (spec % TYPE('a) % Q % x %% prfa %% prf')))",
   1.181 +   \<open>(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %%
   1.182 +      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.183 +      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.184 +    (allI % TYPE('a) % P %% prfa %%
   1.185 +      (Lam x.
   1.186 +          iffD2 % P x % Q x %% (prf % x) %%
   1.187 +           (spec % TYPE('a) % Q % x %% prfa %% prf')))\<close>,
   1.188  
   1.189     (* Ex *)
   1.190  
   1.191 -   "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   1.192 - \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   1.193 - \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   1.194 - \  (exE % TYPE('a) % P % \<exists>x. Q x %% prfa %% prf' %%  \
   1.195 - \    (Lam x H : P x.  \
   1.196 - \        exI % TYPE('a) % Q % x %% prfa %%  \
   1.197 - \         (iffD1 % P x % Q x %% (prf % x) %% H)))",
   1.198 +   \<open>(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%
   1.199 +      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.200 +      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.201 +    (exE % TYPE('a) % P % \<exists>x. Q x %% prfa %% prf' %%
   1.202 +      (Lam x H : P x.
   1.203 +          exI % TYPE('a) % Q % x %% prfa %%
   1.204 +           (iffD1 % P x % Q x %% (prf % x) %% H)))\<close>,
   1.205  
   1.206 -   "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%  \
   1.207 - \    (HOL.refl % TYPE('T3) % x1 %% prfT3) %%  \
   1.208 - \    (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==  \
   1.209 - \  (exE % TYPE('a) % Q % \<exists>x. P x %% prfa %% prf' %%  \
   1.210 - \    (Lam x H : Q x.  \
   1.211 - \        exI % TYPE('a) % P % x %% prfa %%  \
   1.212 - \         (iffD2 % P x % Q x %% (prf % x) %% H)))",
   1.213 +   \<open>(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %%
   1.214 +      (HOL.refl % TYPE('T3) % x1 %% prfT3) %%
   1.215 +      (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') ==
   1.216 +    (exE % TYPE('a) % Q % \<exists>x. P x %% prfa %% prf' %%
   1.217 +      (Lam x H : Q x.
   1.218 +          exI % TYPE('a) % P % x %% prfa %%
   1.219 +           (iffD2 % P x % Q x %% (prf % x) %% H)))\<close>,
   1.220  
   1.221     (* \<and> *)
   1.222  
   1.223 -   "(iffD1 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.224 - \    (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%  \
   1.225 - \      (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.226 - \  (conjI % B % D %%  \
   1.227 - \    (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%  \
   1.228 - \    (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
   1.229 +   \<open>(iffD1 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.230 +      (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%
   1.231 +        (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.232 +    (conjI % B % D %%
   1.233 +      (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %%
   1.234 +      (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))\<close>,
   1.235  
   1.236 -   "(iffD2 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.237 - \    (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%  \
   1.238 - \      (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.239 - \  (conjI % A % C %%  \
   1.240 - \    (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%  \
   1.241 - \    (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
   1.242 +   \<open>(iffD2 % A \<and> C % B \<and> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.243 +      (cong % TYPE('T3) % TYPE('T4) % op \<and> % op \<and> % A % B %% prfT3 %% prfT4 %%
   1.244 +        (HOL.refl % TYPE('T5) % op \<and> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.245 +    (conjI % A % C %%
   1.246 +      (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %%
   1.247 +      (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))\<close>,
   1.248  
   1.249 -   "(cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%  \
   1.250 - \    (HOL.refl % TYPE(bool=>bool) % op \<and> A %% prfbb)) ==  \
   1.251 - \  (cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%  \
   1.252 - \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.253 - \      (op \<and> :: bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) % A % A %%  \
   1.254 - \        prfb %% prfbb %%  \
   1.255 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) %%  \
   1.256 - \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   1.257 - \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   1.258 +   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%
   1.259 +      (HOL.refl % TYPE(bool=>bool) % op \<and> A %% prfbb)) ==
   1.260 +    (cong % TYPE(bool) % TYPE(bool) % op \<and> A % op \<and> A % B % C %% prfb %% prfb %%
   1.261 +      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.262 +        (op \<and> :: bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) % A % A %%
   1.263 +          prfb %% prfbb %%
   1.264 +          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<and> :: bool=>bool=>bool) %%
   1.265 +             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.266 +          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.267  
   1.268     (* \<or> *)
   1.269  
   1.270 -   "(iffD1 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.271 - \    (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%  \
   1.272 - \      (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.273 - \  (disjE % A % C % B \<or> D %% prf3 %%  \
   1.274 - \    (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%  \
   1.275 - \    (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
   1.276 +   \<open>(iffD1 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.277 +      (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%
   1.278 +        (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.279 +    (disjE % A % C % B \<or> D %% prf3 %%
   1.280 +      (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %%
   1.281 +      (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))\<close>,
   1.282  
   1.283 -   "(iffD2 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.284 - \    (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%  \
   1.285 - \      (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.286 - \  (disjE % B % D % A \<or> C %% prf3 %%  \
   1.287 - \    (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%  \
   1.288 - \    (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
   1.289 +   \<open>(iffD2 % A \<or> C % B \<or> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.290 +      (cong % TYPE('T3) % TYPE('T4) % op \<or> % op \<or> % A % B %% prfT3 %% prfT4 %%
   1.291 +        (HOL.refl % TYPE('T5) % op \<or> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.292 +    (disjE % B % D % A \<or> C %% prf3 %%
   1.293 +      (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %%
   1.294 +      (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))\<close>,
   1.295  
   1.296 -   "(cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%  \
   1.297 - \    (HOL.refl % TYPE(bool=>bool) % op \<or> A %% prfbb)) ==  \
   1.298 - \  (cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%  \
   1.299 - \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.300 - \      (op \<or> :: bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) % A % A %%  \
   1.301 - \        prfb %% prfbb %%  \
   1.302 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) %%  \
   1.303 - \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   1.304 - \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   1.305 +   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%
   1.306 +      (HOL.refl % TYPE(bool=>bool) % op \<or> A %% prfbb)) ==
   1.307 +    (cong % TYPE(bool) % TYPE(bool) % op \<or> A % op \<or> A % B % C %% prfb %% prfb %%
   1.308 +      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.309 +        (op \<or> :: bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) % A % A %%
   1.310 +          prfb %% prfbb %%
   1.311 +          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<or> :: bool=>bool=>bool) %%
   1.312 +             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.313 +          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.314  
   1.315     (* \<longrightarrow> *)
   1.316  
   1.317 -   "(iffD1 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.318 - \    (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%  \
   1.319 - \      (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.320 - \  (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%  \
   1.321 - \    (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
   1.322 +   \<open>(iffD1 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.323 +      (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%
   1.324 +        (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.325 +    (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %%
   1.326 +      (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))\<close>,
   1.327  
   1.328 -   "(iffD2 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%  \
   1.329 - \    (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%  \
   1.330 - \      (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==  \
   1.331 - \  (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%  \
   1.332 - \    (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
   1.333 +   \<open>(iffD2 % A \<longrightarrow> C % B \<longrightarrow> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %%
   1.334 +      (cong % TYPE('T3) % TYPE('T4) % op \<longrightarrow> % op \<longrightarrow> % A % B %% prfT3 %% prfT4 %%
   1.335 +        (HOL.refl % TYPE('T5) % op \<longrightarrow> %% prfT5) %% prf1) %% prf2) %% prf3) ==
   1.336 +    (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %%
   1.337 +      (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))\<close>,
   1.338  
   1.339 -   "(cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%  \
   1.340 - \    (HOL.refl % TYPE(bool=>bool) % op \<longrightarrow> A %% prfbb)) ==  \
   1.341 - \  (cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%  \
   1.342 - \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.343 - \      (op \<longrightarrow> :: bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) % A % A %%  \
   1.344 - \        prfb %% prfbb %%  \
   1.345 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) %%  \
   1.346 - \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   1.347 - \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   1.348 +   \<open>(cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%
   1.349 +      (HOL.refl % TYPE(bool=>bool) % op \<longrightarrow> A %% prfbb)) ==
   1.350 +    (cong % TYPE(bool) % TYPE(bool) % op \<longrightarrow> A % op \<longrightarrow> A % B % C %% prfb %% prfb %%
   1.351 +      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.352 +        (op \<longrightarrow> :: bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) % A % A %%
   1.353 +          prfb %% prfbb %%
   1.354 +          (HOL.refl % TYPE(bool=>bool=>bool) % (op \<longrightarrow> :: bool=>bool=>bool) %%
   1.355 +             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.356 +          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.357  
   1.358     (* \<not> *)
   1.359  
   1.360 -   "(iffD1 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   1.361 - \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   1.362 - \  (notI % Q %% (Lam H: Q.  \
   1.363 - \    notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
   1.364 +   \<open>(iffD1 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%
   1.365 +      (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==
   1.366 +    (notI % Q %% (Lam H: Q.
   1.367 +      notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))\<close>,
   1.368  
   1.369 -   "(iffD2 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%  \
   1.370 - \    (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==  \
   1.371 - \  (notI % P %% (Lam H: P.  \
   1.372 - \    notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
   1.373 +   \<open>(iffD2 % \<not> P % \<not> Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %%
   1.374 +      (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) ==
   1.375 +    (notI % P %% (Lam H: P.
   1.376 +      notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))\<close>,
   1.377  
   1.378     (* = *)
   1.379  
   1.380 -   "(iffD1 % B % D %%  \
   1.381 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   1.382 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   1.383 - \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.384 - \  (iffD1 % C % D %% prf2 %%  \
   1.385 - \    (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
   1.386 +   \<open>(iffD1 % B % D %%
   1.387 +      (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.388 +        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.389 +          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.390 +    (iffD1 % C % D %% prf2 %%
   1.391 +      (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))\<close>,
   1.392  
   1.393 -   "(iffD2 % B % D %%  \
   1.394 - \    (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   1.395 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   1.396 - \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.397 - \  (iffD1 % A % B %% prf1 %%  \
   1.398 - \    (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
   1.399 +   \<open>(iffD2 % B % D %%
   1.400 +      (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.401 +        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.402 +          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.403 +    (iffD1 % A % B %% prf1 %%
   1.404 +      (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))\<close>,
   1.405  
   1.406 -   "(iffD1 % A % C %%  \
   1.407 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   1.408 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   1.409 - \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==  \
   1.410 - \  (iffD2 % C % D %% prf2 %%  \
   1.411 - \    (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
   1.412 +   \<open>(iffD1 % A % C %%
   1.413 +      (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.414 +        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.415 +          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)==
   1.416 +    (iffD2 % C % D %% prf2 %%
   1.417 +      (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))\<close>,
   1.418  
   1.419 -   "(iffD2 % A % C %%  \
   1.420 - \    (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%  \
   1.421 - \      (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%  \
   1.422 - \        (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==  \
   1.423 - \  (iffD2 % A % B %% prf1 %%  \
   1.424 - \    (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
   1.425 +   \<open>(iffD2 % A % C %%
   1.426 +      (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %%
   1.427 +        (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %%
   1.428 +          (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) ==
   1.429 +    (iffD2 % A % B %% prf1 %%
   1.430 +      (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))\<close>,
   1.431  
   1.432 -   "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   1.433 - \    (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==  \
   1.434 - \  (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%  \
   1.435 - \    (cong % TYPE(bool) % TYPE(bool=>bool) %  \
   1.436 - \      (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%  \
   1.437 - \        prfb %% prfbb %%  \
   1.438 - \        (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%  \
   1.439 - \           (OfClass type_class % TYPE(bool=>bool=>bool))) %%  \
   1.440 - \        (HOL.refl % TYPE(bool) % A %% prfb)))",
   1.441 +   \<open>(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%
   1.442 +      (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) ==
   1.443 +    (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %%
   1.444 +      (cong % TYPE(bool) % TYPE(bool=>bool) %
   1.445 +        (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %%
   1.446 +          prfb %% prfbb %%
   1.447 +          (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %%
   1.448 +             (OfClass type_class % TYPE(bool=>bool=>bool))) %%
   1.449 +          (HOL.refl % TYPE(bool) % A %% prfb)))\<close>,
   1.450  
   1.451     (** transitivity, reflexivity, and symmetry **)
   1.452  
   1.453 -   "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   1.454 - \  (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
   1.455 +   \<open>(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==
   1.456 +    (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))\<close>,
   1.457  
   1.458 -   "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==  \
   1.459 - \  (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
   1.460 +   \<open>(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) ==
   1.461 +    (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))\<close>,
   1.462  
   1.463 -   "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   1.464 +   \<open>(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf\<close>,
   1.465  
   1.466 -   "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf",
   1.467 +   \<open>(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf\<close>,
   1.468  
   1.469 -   "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)",
   1.470 +   \<open>(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)\<close>,
   1.471  
   1.472 -   "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)",
   1.473 +   \<open>(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)\<close>,
   1.474  
   1.475     (** normalization of HOL proofs **)
   1.476  
   1.477 -   "(mp % A % B %% (impI % A % B %% prf)) == prf",
   1.478 +   \<open>(mp % A % B %% (impI % A % B %% prf)) == prf\<close>,
   1.479  
   1.480 -   "(impI % A % B %% (mp % A % B %% prf)) == prf",
   1.481 +   \<open>(impI % A % B %% (mp % A % B %% prf)) == prf\<close>,
   1.482  
   1.483 -   "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x",
   1.484 +   \<open>(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x\<close>,
   1.485  
   1.486 -   "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf",
   1.487 +   \<open>(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf\<close>,
   1.488  
   1.489 -   "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)",
   1.490 +   \<open>(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)\<close>,
   1.491  
   1.492 -   "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf",
   1.493 +   \<open>(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf\<close>,
   1.494  
   1.495 -   "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
   1.496 +   \<open>(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)\<close>,
   1.497  
   1.498 -   "(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
   1.499 +   \<open>(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)\<close>,
   1.500  
   1.501 -   "(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
   1.502 +   \<open>(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1\<close>,
   1.503  
   1.504 -   "(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
   1.505 +   \<open>(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2\<close>,
   1.506  
   1.507 -   "(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
   1.508 +   \<open>(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1\<close>,
   1.509  
   1.510 -   "(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
   1.511 +   \<open>(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2\<close>];
   1.512  
   1.513  
   1.514  (** Replace congruence rules by substitution rules **)