# HG changeset patch # User berghofe # Date 1238675969 -7200 # Node ID a218363290c33ac961bdb02b17fd5c595782069a # Parent 0e5ec6d2c1d95abea0372b5c2c8900d588423afe# Parent 5e20f9c2008618fd6936f97e3d211af89b3dd687 merged diff -r 0e5ec6d2c1d9 -r a218363290c3 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Apr 02 14:09:41 2009 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Thu Apr 02 14:39:29 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/rewrite_hol_proof.ML - ID: $Id$ Author: Stefan Berghofer, TU Muenchen Rewrite rules for HOL proofs @@ -71,7 +70,7 @@ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", + \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))", "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ @@ -85,7 +84,7 @@ \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", + \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))", (** rewriting on bool: insert proper congruence rules for logical connectives **)