--- a/NEWS Thu Mar 27 12:06:26 2008 +0100
+++ b/NEWS Thu Mar 27 14:41:06 2008 +0100
@@ -29,6 +29,8 @@
*** Pure ***
+* Eliminated theory ProtoPure. Potential INCOMPATIBILITY.
+
* Instantiation target allows for simultaneous specification of class
instance operations together with an instantiation proof.
Type-checking phase allows to refer to class operations uniformly.
@@ -44,6 +46,9 @@
*** HOL ***
+* HOL (and FOL): renamed variables in rules imp_elim and swap.
+Potential INCOMPATIBILITY.
+
* Theory Product_Type: duplicated lemmas split_Pair_apply and injective_fst_snd
removed, use split_eta and prod_eqI instead. Renamed upd_fst to apfst and upd_snd
to apsnd. INCOMPATIBILITY.