# HG changeset patch
# User haftmann
# Date 1159270455 -7200
# Node ID b3cd1233167fa4a72d3f01f325c933e89534cb9e
# Parent  8b52cdaee86cc5cf5a4b5012209eb2b5389ae8b3
renamed 0 and 1 to HOL.zero and HOL.one respectivly

diff -r 8b52cdaee86c -r b3cd1233167f NEWS
--- 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.