- Proofs are now hidden by default when generating documents
authorberghofe
Thu Jan 27 12:37:02 2005 +0100 (2005-01-27)
changeset 15475fdf9434b04ea
parent 15474 6e60be6a6c21
child 15476 b8cb20cc0c0b
- 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)
NEWS
     1.1 --- a/NEWS	Thu Jan 27 12:35:20 2005 +0100
     1.2 +++ b/NEWS	Thu Jan 27 12:37:02 2005 +0100
     1.3 @@ -25,6 +25,9 @@
     1.4    will still be supported for some time but will eventually disappear.
     1.5    The syntax of old-style theories has not changed.
     1.6  
     1.7 +* Theory loader: parent theories can now also be referred to via
     1.8 +  relative and absolute paths.
     1.9 +
    1.10  * Provers/quasi.ML:  new transitivity reasoners for transitivity only
    1.11    and quasi orders.
    1.12  
    1.13 @@ -79,6 +82,9 @@
    1.14  * Pure: tuned internal renaming of symbolic identifiers -- attach
    1.15    primes instead of base 26 numbers.
    1.16  
    1.17 +* Pure: new flag show_var_qmarks to control printing of leading
    1.18 +  question marks of variable names.
    1.19 +
    1.20  * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
    1.21  
    1.22  * Pure/Syntax: pretty pinter now supports unbreakable blocks,
    1.23 @@ -142,9 +148,10 @@
    1.24  
    1.25  * Document preparation: Proof scripts as well as some other commands
    1.26    such as ML or parse/print_translation can now be hidden in the document.
    1.27 -  Hiding can be enabled either via the option '-H true' of isatool usedir
    1.28 -  or by setting the reference variable IsarOutput.hide_commands. Additional
    1.29 -  commands to be hidden may be declared using IsarOutput.add_hidden_commands.
    1.30 +  Hiding is enabled by default, and can be disabled either via the option
    1.31 +  '-H true' of isatool usedir or by resetting the reference variable
    1.32 +  IsarOutput.hide_commands. Additional commands to be hidden may be
    1.33 +  declared using IsarOutput.add_hidden_commands.
    1.34  
    1.35  * ML: output via the Isabelle channels of writeln/warning/error
    1.36    etc. is now passed through Output.output, with a hook for arbitrary
    1.37 @@ -169,7 +176,14 @@
    1.38    - "includes" disallowed in declaration of named locales (command "locale").
    1.39    - Fixed parameter management in theorem generation for goals with "includes".
    1.40      INCOMPATIBILITY: rarely, the generated theorem statement is different.
    1.41 - 
    1.42 +
    1.43 +* New syntax
    1.44 +
    1.45 +    <theorem_name> (<index>, ..., <index>-<index>, ...)
    1.46 +
    1.47 +  for referring to specific theorems in a named list of theorems via
    1.48 +  indices.
    1.49 +
    1.50  *** HOL ***
    1.51  
    1.52  * Datatype induction via method `induct' now preserves the name of the