NEWS
changeset 49972 f11f8905d9fd
parent 49968 d9e08e2555f9
child 50020 6b9611abcd4c
--- a/NEWS	Mon Oct 22 19:02:36 2012 +0200
+++ b/NEWS	Mon Oct 22 22:24:34 2012 +0200
@@ -99,6 +99,9 @@
 
 *** HOL ***
 
+* Removed constant "chars".  Prefer "Enum.enum" on type "char"
+directly.  INCOMPATIBILITY.
+
 * Moved operation product, sublists and n_lists from Enum.thy
 to List.thy.  INCOMPATIBILITY.