renamed 0 and 1 to HOL.zero and HOL.one respectivly

--- a/NEWS	Tue Sep 26 11:11:57 2006 +0200
+++ b/NEWS	Tue Sep 26 13:34:15 2006 +0200
@@ -471,6 +471,12 @@
 
 *** HOL ***
 
+* Renamed constants in HOL.thy:
+    0      ~> HOL.zero
+    1      ~> HOL.one
+INCOMPATIBILITY: ML code directly refering to constant names may need adaption
+This in general only affects hand-written proof tactics, simprocs and so on.
+
 * New theory OperationalEquality providing class 'eq' with constant 'eq',
 allowing for code generation with polymorphic equality.