--- a/NEWS Wed Mar 05 12:24:52 2008 +0100
+++ b/NEWS Wed Mar 05 14:14:50 2008 +0100
@@ -34,6 +34,9 @@
*** HOL ***
+* Library/RBT.thy: New theory of red-black trees, an efficient
+implementation of finite maps.
+
* Theory Int: The representation of numerals has changed. The infix
operator BIT and the bit datatype with constructors B0 and B1 have
disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
@@ -110,6 +113,26 @@
with multithreading.
+*** ZF ***
+
+* Renamed theories:
+
+ Datatype.thy -> Datatype_ZF.thy
+ Inductive.thy -> Inductive_ZF.thy
+ Int.thy -> Int_ZF.thy
+ IntDiv.thy -> IntDiv_ZF.thy
+ Nat.thy -> Nat_ZF.thy
+ List.thy -> List_ZF.thy
+ Main.thy -> Main_ZF.thy
+
+ This is to allow to load both ZF and HOL in the same session.
+
+ INCOMPATIBILITY: ZF theories that import individual theories below
+ Main might need to be adapted. For compatibility, a new
+ "theory Main imports Main_ZF begin end" is provided, so if you just
+ imported "Main", no changes are needed.
+
+
*** ML ***
* ML within Isar: antiquotation @{const name} or @{const