--- 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]);