- Proofs are now hidden by default when generating documents
- New syntax for referring to theorems in lists
- Improvements to theory loader (relative and absolute paths)

--- a/NEWS	Thu Jan 27 12:35:20 2005 +0100
+++ b/NEWS	Thu Jan 27 12:37:02 2005 +0100
@@ -25,6 +25,9 @@
   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.
 
@@ -79,6 +82,9 @@
 * 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,
@@ -142,9 +148,10 @@
 
 * 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
@@ -169,7 +176,14 @@
   - "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