changeset 20712 | b3cd1233167f |
parent 20620 | 8b26f58c5646 |
child 20716 | a6686a8e1b68 |
--- 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.