NEWS

   value is true.
 
 * Pure: tuned internal renaming of symbolic identifiers -- attach
   primes instead of base 26 numbers.
 
-* Pure: new flag show_var_qmarks to control printing of leading
-  question marks of variable names.
+* Pure: new flag show_question_marks controls printing of leading
+  question marks in schematic variable names.
 
 * Pure: new version of thms_containing that searches for a list 
   of patterns instead of a list of constants. Available in 
   ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. 
   Example search: "(_::nat) + _ + _"   "_ ==> _"

   space; use isatool fixcpure to adapt your theory and ML sources.
 
 
 *** Document preparation ***
 
-* New antiquotation @{term_type term} printing a term with its
-  type annotated
-
-* New antiquotation @{typeof term} printing the - surprise - the type of 
-  a term
-
-* New antiquotation @{const const} which is the same as @{term const} except
-  that const must be a defined constant identifier; helpful for early detection
-  of typoes
-
-* Two new antiquotations @{term_style style term} and @{thm_style style thm}
-  which print a term / theorem applying a "style" to it; predefined styles
-  are "lhs" and "rhs" printing the lhs/rhs of definitions, equations,
-  inequations etc. and "conclusion" printing only the conclusion of a theorem.
-  More styles may be defined using ML; see the "LaTeX Sugar" document for more
+* Several new antiquotation:
+
+  @{term_type term} prints a term with its type annotated;
+
+  @{typeof term} prints the type of a term;
+
+  @{const const} is the same as @{term const}, but checks
+    that the argument is a known logical constant;
+
+  @{term_style style term} and @{thm_style style thm} print a term or
+    theorem applying a "style" to it
+
+  Predefined styles are "lhs" and "rhs" printing the lhs/rhs of
+  definitions, equations, inequations etc. and "conclusion" printing
+  only the conclusion of a meta-logical statement theorem.  Styles may
+  be defined via TermStyle.add_style in ML.  See the "LaTeX Sugar"
+  document for more information.
 
 * Antiquotations now provide the option 'locale=NAME' to specify an
   alternative context used for evaluating and printing the subsequent
   argument, as in @{thm [locale=LC] fold_commute}, for example.
 

   and x-symbol; use option '-m epsilon' to get it actually printed.
   Moreover, the mathematically important symbolic identifier
   \<epsilon> becomes available as variable, constant etc.
 
 * HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
-  Similarly for all quantifiers: "ALL x > y" etc.
-  The x-symbol for >= is \<ge>.
-
-* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
-           (and similarly for "\<in>" instead of ":")
+  Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
+  is \<ge>.
+
+* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for
+  "\<in>" instead of ":").
 
 * HOL/SetInterval: The syntax for open intervals has changed:
 
   Old         New
   {..n(}   -> {..<n}