NEWS
changeset 55547 384bfd19ee61
parent 55536 56ebc4d4d008
child 55580 d12a13713cb4
     1.1 --- a/NEWS	Mon Feb 17 21:37:41 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 17 22:39:20 2014 +0100
     1.3 @@ -358,6 +358,13 @@
     1.4  pass runtime Proof.context (and ensure that the simplified entity
     1.5  actually belongs to it).
     1.6  
     1.7 +* Subtle change of semantics of Thm.eq_thm: theory stamps are not
     1.8 +compared (according to Thm.thm_ord), but assumed to be covered by the
     1.9 +current background theory.  Thus equivalent data produced in different
    1.10 +branches of the theory graph usually coincides (e.g. relevant for
    1.11 +theory merge).  Note that the softer Thm.eq_thm_prop is often more
    1.12 +appropriate than Thm.eq_thm.
    1.13 +
    1.14  
    1.15  *** System ***
    1.16