1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Thu Apr 02 14:09:41 2009 +0200
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Thu Apr 02 14:39:29 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/rewrite_hol_proof.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7  
     1.8  Rewrite rules for HOL proofs
     1.9 @@ -71,7 +70,7 @@
    1.10   \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.11   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.12   \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.13 - \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.14 + \    (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))",
    1.15  
    1.16     "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %%  \
    1.17   \    (axm.symmetric % TYPE('T2) % x5 % x6 %%  \
    1.18 @@ -85,7 +84,7 @@
    1.19   \        (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %%  \
    1.20   \        (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %%  \
    1.21   \      (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %%  \
    1.22 - \    (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))",
    1.23 + \    (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))",
    1.24  
    1.25     (** rewriting on bool: insert proper congruence rules for logical connectives **)
    1.26