--- a/src/Pure/drule.ML Sat Jan 28 17:28:53 2006 +0100
+++ b/src/Pure/drule.ML Sat Jan 28 17:28:54 2006 +0100
@@ -65,6 +65,7 @@
val transitive_thm: thm
val symmetric_fun: thm -> thm
val extensional: thm -> thm
+ val equals_cong: thm
val imp_cong: thm
val swap_prems_eq: thm
val equal_abs_elim: cterm -> thm -> thm
@@ -627,6 +628,9 @@
abstract_rule "x" (snd (Thm.dest_comb (fst (dest_equals (cprop_of eq))))) eq
in equal_elim (eta_conversion (cprop_of eq')) eq' end;
+val equals_cong =
+ store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y"));
+
val imp_cong =
let
val ABC = read_prop "PROP A ==> PROP B == PROP C"