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