# HG changeset patch
# User wenzelm
# Date 1206625266 -3600
# Node ID d5883907c5147cff68374d3ebd554acb65294df6
# Parent  3dfb36923a567c6d48d5dd8df87a9d679616436f
HOL (and FOL): renamed variables in rules imp_elim and swap;
Eliminated theory ProtoPure.

diff -r 3dfb36923a56 -r d5883907c514 NEWS
--- 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.