HOL (and FOL): renamed variables in rules imp_elim and swap;
Eliminated theory ProtoPure.

--- 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.