--- a/NEWS Mon Nov 07 12:08:22 2011 +0100
+++ b/NEWS Mon Nov 07 14:14:20 2011 +0100
@@ -10,22 +10,24 @@
instead. INCOMPATIBILITY.
* Ancient code generator for SML and its commands 'code_module',
- 'code_library', 'consts_code', 'types_code' have been discontinued.
- Use commands of the generic code generator instead. INCOMPATIBILITY.
-
-* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
-instead. INCOMPATIBILITY.
+'code_library', 'consts_code', 'types_code' have been discontinued.
+Use commands of the generic code generator instead. INCOMPATIBILITY.
+
+* Redundant attribute 'code_inline' has been discontinued. Use
+'code_unfold' instead. INCOMPATIBILITY.
+
*** HOL ***
-* 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
-
-* 'Set.not_member' now qualifed. INCOMPATIBILITY.
-
-* 'sublists' moved to More_List.thy. INCOMPATIBILITY.
+* "Transitive_Closure.ntrancl": bounded transitive closure on
+relations.
+
+* Constant "Set.not_member" now qualifed. INCOMPATIBILITY.
+
+* "sublists" moved to theory More_List. INCOMPATIBILITY.
* Theory Int: Discontinued many legacy theorems specific to type int.
- INCOMPATIBILITY, use the corresponding generic theorems instead.
+INCOMPATIBILITY, use the corresponding generic theorems instead.
zminus_zminus ~> minus_minus
zminus_0 ~> minus_zero
@@ -62,17 +64,18 @@
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
zero_le_zpower_abs ~> zero_le_power_abs
-* New case_product attribute to generate a case rule doing multiple case
- distinctions at the same time: E.g.
-
- list.exhaust[case_product nat.exhaust]
-
- produces a rule which can be used to perform case distinction on both
- a list and a nat.
+* New "case_product" attribute to generate a case rule doing multiple
+case distinctions at the same time. E.g.
+
+ list.exhaust [case_product nat.exhaust]
+
+produces a rule which can be used to perform case distinction on both
+a list and a nat.
+
*** FOL ***
-* New case_product attribute (see HOL).
+* New "case_product" attribute (see HOL).
*** ML ***