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