NEWS

 
   theory <name> = <theory1> + ... + <theoryn>:
 
   will still be supported for some time but will eventually disappear.
   The syntax of old-style theories has not changed.
+
+* Theory loader: parent theories can now also be referred to via
+  relative and absolute paths.
 
 * Provers/quasi.ML:  new transitivity reasoners for transitivity only
   and quasi orders.
 
 * Provers/trancl.ML:  new transitivity reasoner for transitive and

   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/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,
   specified in mixfix annotations as "(00...)".
 

   these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
   respectively.
 
 * Document preparation: Proof scripts as well as some other commands
   such as ML or parse/print_translation can now be hidden in the document.
-  Hiding can be enabled either via the option '-H true' of isatool usedir
-  or by setting the reference variable IsarOutput.hide_commands. Additional
-  commands to be hidden may be declared using IsarOutput.add_hidden_commands.
+  Hiding is enabled by default, and can be disabled either via the option
+  '-H true' of isatool usedir or by resetting the reference variable
+  IsarOutput.hide_commands. Additional commands to be hidden may be
+  declared using IsarOutput.add_hidden_commands.
 
 * ML: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --
   the first active mode that provides a output function wins).

 
 * Locales:
   - "includes" disallowed in declaration of named locales (command "locale").
   - Fixed parameter management in theorem generation for goals with "includes".
     INCOMPATIBILITY: rarely, the generated theorem statement is different.
- 
+
+* New syntax
+
+    <theorem_name> (<index>, ..., <index>-<index>, ...)
+
+  for referring to specific theorems in a named list of theorems via
+  indices.
+
 *** HOL ***
 
 * Datatype induction via method `induct' now preserves the name of the
   induction variable. For example, when proving P(xs::'a list) by induction
   on xs, the induction step is now P(xs) ==> P(a#xs) rather than