src/HOL/simpdata.ML
changeset 1548 afe750876848
parent 1485 240cc98b94a7
child 1655 5be64540f275
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 05 17:37:28 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 06 10:05:00 1996 +0100
     1.3 @@ -143,6 +143,10 @@
     1.4      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
     1.5          (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
     1.6  
     1.7 +val rev_conj_cong = impI RSN
     1.8 +    (2, prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
     1.9 +        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
    1.10 +
    1.11  (** 'if' congruence rules: neither included by default! *)
    1.12  
    1.13  (*Simplifies x assuming c and y assuming ~c*)