--- a/NEWS Mon Feb 17 21:37:41 2014 +0100
+++ b/NEWS Mon Feb 17 22:39:20 2014 +0100
@@ -358,6 +358,13 @@
pass runtime Proof.context (and ensure that the simplified entity
actually belongs to it).
+* Subtle change of semantics of Thm.eq_thm: theory stamps are not
+compared (according to Thm.thm_ord), but assumed to be covered by the
+current background theory. Thus equivalent data produced in different
+branches of the theory graph usually coincides (e.g. relevant for
+theory merge). Note that the softer Thm.eq_thm_prop is often more
+appropriate than Thm.eq_thm.
+
*** System ***