# HG changeset patch
# User wenzelm
# Date 1138465734 -3600
# Node ID 24dcd5b0e26b3247794792b7c5bc34551bf65271
# Parent  67f9347ea21d44a03053cf40b7c85e4005954449
added equals_cong;

diff -r 67f9347ea21d -r 24dcd5b0e26b src/Pure/drule.ML
--- 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"