# HG changeset patch
# User paulson
# Date 867058235 -7200
# Node ID 5ff4bfab859cd53e7edcd4196462d23bc5e52e68
# Parent  a8ab7c64817c785e0fae3520dba58987c123b11d
Removal of COND_CONG, which is just if_cong RS eq_reflection

diff -r a8ab7c64817c -r 5ff4bfab859c TFL/thms.sig
--- a/TFL/thms.sig	Mon Jun 23 10:42:03 1997 +0200
+++ b/TFL/thms.sig	Mon Jun 23 11:30:35 1997 +0200
@@ -12,7 +12,6 @@
    val CUT_LEMMA       :thm
    val SELECT_AX       :thm
    
-   val COND_CONG :thm
    val LET_CONG  :thm
 
    val eqT       :thm
diff -r a8ab7c64817c -r 5ff4bfab859c TFL/thms.sml
--- a/TFL/thms.sml	Mon Jun 23 10:42:03 1997 +0200
+++ b/TFL/thms.sml	Mon Jun 23 11:30:35 1997 +0200
@@ -19,7 +19,7 @@
    end;
 
   (*-------------------------------------------------------------------------
-   *  A useful congruence rule
+   *  Congruence rule needed for TFL, but not for general simplification
    *-------------------------------------------------------------------------*)
    local val [p1,p2] = goal HOL.thy "(M = N) ==> \
                           \ (!!x. ((x = N) ==> (f x = g x))) ==> \
@@ -27,10 +27,7 @@
          val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
          val _ = by (rtac p2 1);
          val _ = by (rtac refl 1);
-   in val LET_CONG = result() RS eq_reflection
-   end;
-
-   val COND_CONG = if_cong RS eq_reflection;
+   in val LET_CONG = result() end;
 
    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);