src/HOL/Tools/rewrite_hol_proof.ML
changeset 28712 4f2954d995f0
parent 28262 aa7ca36d67fd
child 28801 fc45401bdf6f
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 31 10:35:30 2008 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Oct 31 10:37:34 2008 +0100
     1.3 @@ -23,15 +23,15 @@
     1.4  
     1.5    ["(equal_elim % x1 % x2 %% \
     1.6   \    (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %%  \
     1.7 - \      (axm.reflexive % TYPE('T3) % x4) %% prf1) %% prf2) ==  \
     1.8 + \      (axm.reflexive % TYPE('T3) % x4) %% prf1)) ==  \
     1.9   \  (iffD1 % A % B %%  \
    1.10 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
    1.11 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    1.12  
    1.13     "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %%  \
    1.14   \    (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %%  \
    1.15 - \      (axm.reflexive % TYPE('T4) % x6) %% prf1)) %% prf2) ==  \
    1.16 + \      (axm.reflexive % TYPE('T4) % x6) %% prf1))) ==  \
    1.17   \  (iffD2 % A % B %%  \
    1.18 - \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1) %% prf2)",
    1.19 + \    (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
    1.20  
    1.21     "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %%  \
    1.22   \    (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) ==  \