# HG changeset patch
# User wenzelm
# Date 1320671660 -3600
# Node ID bf6add30ab20640e15f5a8353cf93cc7ddfd30e2
# Parent  3a9f84ad31e7115ba1ebde0a4171f6d46d7c0bbf
misc tuning;

diff -r 3a9f84ad31e7 -r bf6add30ab20 NEWS
--- 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 ***