misc tuning for release;
authorwenzelm
Sat Sep 28 16:10:26 2013 +0200 (2013-09-28)
changeset 53971c4156b37627f
parent 53970 eee1863c565a
child 53972 c6297fa1031a
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Sat Sep 28 15:36:14 2013 +0200
     1.2 +++ b/NEWS	Sat Sep 28 16:10:26 2013 +0200
     1.3 @@ -1,11 +1,18 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2013-1 (November 2013)
    1.10 +-------------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 +* Discontinued obsolete 'uses' within theory header.  Note that
    1.15 +commands like 'ML_file' work without separate declaration of file
    1.16 +dependencies.  Minor INCOMPATIBILITY.
    1.17 +
    1.18 +* Discontinued redundant 'use' command, which was superseded by
    1.19 +'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
    1.20 +
    1.21  * Simplified subscripts within identifiers, using plain \<^sub>
    1.22  instead of the second copy \<^isub> and \<^isup>.  Superscripts are
    1.23  only for literal tokens within notation; explicit mixfix annotations
    1.24 @@ -29,23 +36,6 @@
    1.25  * Renamed command 'print_configs' to 'print_options'.  Minor
    1.26  INCOMPATIBILITY.
    1.27  
    1.28 -* Sessions may be organized via 'chapter' specifications in the ROOT
    1.29 -file, which determines a two-level hierarchy of browser info.  The old
    1.30 -tree-like organization via implicit sub-session relation, with its
    1.31 -tendency towards erratic fluctuation of URLs, has been discontinued.
    1.32 -The default chapter is "Unsorted".  Potential INCOMPATIBILITY for HTML
    1.33 -presentation of theories.
    1.34 -
    1.35 -* Discontinued obsolete 'uses' within theory header.  Note that
    1.36 -commands like 'ML_file' work without separate declaration of file
    1.37 -dependencies.  Minor INCOMPATIBILITY.
    1.38 -
    1.39 -* Discontinued redundant 'use' command, which was superseded by
    1.40 -'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.
    1.41 -
    1.42 -* Updated and extended "isar-ref" and "implementation" manual,
    1.43 -eliminated old "ref" manual.
    1.44 -
    1.45  * Proper diagnostic command 'print_state'.  Old 'pr' (with its
    1.46  implicit change of some global references) is retained for now as
    1.47  control command, e.g. for ProofGeneral 3.7.x.
    1.48 @@ -54,40 +44,21 @@
    1.49  and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
    1.50  'display_drafts' instead and print via the regular document viewer.
    1.51  
    1.52 +* Updated and extended "isar-ref" and "implementation" manual,
    1.53 +eliminated old "ref" manual.
    1.54 +
    1.55  
    1.56  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.57  
    1.58 -* File specifications in jEdit (e.g. file browser) may refer to
    1.59 -$ISABELLE_HOME on all platforms.  Discontinued obsolete
    1.60 -$ISABELLE_HOME_WINDOWS variable.
    1.61 -
    1.62 -* Improved support of native Mac OS X functionality.
    1.63 -
    1.64 -* Separate manual "jedit" for Isabelle/jEdit, see isabelle doc or
    1.65 +* New manual "jedit" for Isabelle/jEdit, see isabelle doc or
    1.66  Documentation panel.
    1.67  
    1.68 -* Improved "Theories" panel: Continuous checking of proof document
    1.69 -(visible and required parts) may be controlled explicitly, using check
    1.70 -box or shortcut "C+e ENTER".  Individual theory nodes may be marked
    1.71 -explicitly as required and checked in full, using check box or
    1.72 -shortcut "C+e SPACE".
    1.73 -
    1.74 -* Strictly monotonic document update, without premature cancelation of
    1.75 -running transactions that are still needed: avoid reset/restart of
    1.76 -such command executions while editing.
    1.77 -
    1.78 -* Support for asynchronous print functions, as overlay to existing
    1.79 -document content.
    1.80 -
    1.81 -* Support for automatic tools in HOL, which try to prove or disprove
    1.82 -toplevel theorem statements.
    1.83 +* Dockable window "Documentation" provides access to Isabelle
    1.84 +documentation.
    1.85  
    1.86  * Dockable window "Find" provides query operations for formal entities
    1.87  (GUI front-end to 'find_theorems' command).
    1.88  
    1.89 -* Dockable window "Documentation" provides access to Isabelle
    1.90 -documentation.
    1.91 -
    1.92  * Dockable window "Sledgehammer" manages asynchronous / parallel
    1.93  sledgehammer runs over existing document sources, independently of
    1.94  normal editing and checking process.
    1.95 @@ -95,17 +66,20 @@
    1.96  * Dockable window "Timing" provides an overview of relevant command
    1.97  timing information.
    1.98  
    1.99 -* Action isabelle.reset-font-size resets main text area font size
   1.100 -according to Isabelle/Scala plugin option "jedit_font_reset_size"
   1.101 -(cf. keyboard shortcut C+0).
   1.102 -
   1.103 -* Improved support for Linux look-and-feel "GTK+", see also "Utilities
   1.104 -/ Global Options / Appearance".
   1.105 +* Improved dockable window "Theories": Continuous checking of proof
   1.106 +document (visible and required parts) may be controlled explicitly,
   1.107 +using check box or shortcut "C+e ENTER".  Individual theory nodes may
   1.108 +be marked explicitly as required and checked in full, using check box
   1.109 +or shortcut "C+e SPACE".
   1.110 +
   1.111 +* Strictly monotonic document update, without premature cancellation of
   1.112 +running transactions that are still needed: avoid reset/restart of
   1.113 +such command executions while editing.
   1.114  
   1.115  * Improved completion mechanism, which is now managed by the
   1.116  Isabelle/jEdit plugin instead of SideKick.
   1.117  
   1.118 -  - Various Isabelle plugin options to control popup behaviour and
   1.119 +  - Various Isabelle plugin options to control popup behavior and
   1.120      immediate insertion into buffer.
   1.121  
   1.122    - Light-weight popup, which avoids explicit window (more reactive
   1.123 @@ -134,29 +108,31 @@
   1.124    - Refined table of Isabelle symbol abbreviations (see
   1.125      $ISABELLE_HOME/etc/symbols).
   1.126  
   1.127 +* Support for asynchronous print functions, as overlay to existing
   1.128 +document content.
   1.129 +
   1.130 +* Support for automatic tools in HOL, which try to prove or disprove
   1.131 +toplevel theorem statements.
   1.132 +
   1.133 +* Action isabelle.reset-font-size resets main text area font size
   1.134 +according to Isabelle/Scala plugin option "jedit_font_reset_size"
   1.135 +(cf. keyboard shortcut C+0).
   1.136 +
   1.137 +* File specifications in jEdit (e.g. file browser) may refer to
   1.138 +$ISABELLE_HOME on all platforms.  Discontinued obsolete
   1.139 +$ISABELLE_HOME_WINDOWS variable.
   1.140 +
   1.141 +* Improved support for Linux look-and-feel "GTK+", see also "Utilities
   1.142 +/ Global Options / Appearance".
   1.143 +
   1.144 +* Improved support of native Mac OS X functionality via "MacOSX"
   1.145 +plugin, which is now enabled by default.
   1.146 +
   1.147  
   1.148  *** Pure ***
   1.149  
   1.150 -* Former global reference trace_unify_fail is now available as
   1.151 -configuration option "unify_trace_failure" (global context only).
   1.152 -
   1.153 -* Type theory is now immutable, without any special treatment of
   1.154 -drafts or linear updates (which could lead to "stale theory" errors in
   1.155 -the past).  Discontinued obsolete operations like Theory.copy,
   1.156 -Theory.checkpoint, and the auxiliary type theory_ref.  Minor
   1.157 -INCOMPATIBILITY.
   1.158 -
   1.159 -* System option "proofs" has been discontinued.  Instead the global
   1.160 -state of Proofterm.proofs is persistently compiled into logic images
   1.161 -as required, notably HOL-Proofs.  Users no longer need to change
   1.162 -Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
   1.163 -
   1.164 -* Syntax translation functions (print_translation etc.) always depend
   1.165 -on Proof.context.  Discontinued former "(advanced)" option -- this is
   1.166 -now the default.  Minor INCOMPATIBILITY.
   1.167 -
   1.168  * Target-sensitive commands 'interpretation' and 'sublocale'.
   1.169 -Particulary, 'interpretation' now allows for non-persistent
   1.170 +Particularly, 'interpretation' now allows for non-persistent
   1.171  interpretation within "context ... begin ... end" blocks.  See
   1.172  "isar-ref" manual for details.
   1.173  
   1.174 @@ -169,6 +145,18 @@
   1.175  * Discontinued empty name bindings in 'axiomatization'.
   1.176  INCOMPATIBILITY.
   1.177  
   1.178 +* System option "proofs" has been discontinued.  Instead the global
   1.179 +state of Proofterm.proofs is persistently compiled into logic images
   1.180 +as required, notably HOL-Proofs.  Users no longer need to change
   1.181 +Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
   1.182 +
   1.183 +* Syntax translation functions (print_translation etc.) always depend
   1.184 +on Proof.context.  Discontinued former "(advanced)" option -- this is
   1.185 +now the default.  Minor INCOMPATIBILITY.
   1.186 +
   1.187 +* Former global reference trace_unify_fail is now available as
   1.188 +configuration option "unify_trace_failure" (global context only).
   1.189 +
   1.190  * SELECT_GOAL now retains the syntactic context of the overall goal
   1.191  state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
   1.192  situations.
   1.193 @@ -421,28 +409,28 @@
   1.194  
   1.195  *** ML ***
   1.196  
   1.197 +* Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
   1.198 +"check_property" allows to check specifications of the form "ALL x y
   1.199 +z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
   1.200 +Examples.thy in particular.
   1.201 +
   1.202  * Improved printing of exception trace in Poly/ML 5.5.1, with regular
   1.203  tracing output in the command transaction context instead of physical
   1.204  stdout.  See also Toplevel.debug, Toplevel.debugging and
   1.205  ML_Compiler.exn_trace.
   1.206  
   1.207 -* Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
   1.208 -"check_property" allows to check specifications of the form "ALL x y
   1.209 -z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
   1.210 -Examples.thy in particular.
   1.211 +* ML type "theory" is now immutable, without any special treatment of
   1.212 +drafts or linear updates (which could lead to "stale theory" errors in
   1.213 +the past).  Discontinued obsolete operations like Theory.copy,
   1.214 +Theory.checkpoint, and the auxiliary type theory_ref.  Minor
   1.215 +INCOMPATIBILITY.
   1.216  
   1.217  * More uniform naming of goal functions for skipped proofs:
   1.218  
   1.219      Skip_Proof.prove  ~>  Goal.prove_sorry
   1.220      Skip_Proof.prove_global  ~>  Goal.prove_sorry_global
   1.221  
   1.222 -* Antiquotation @{theory_context A} is similar to @{theory A}, but
   1.223 -presents the result as initial Proof.context.
   1.224 -
   1.225 -* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
   1.226 -operate on Proof.context instead of claset, for uniformity with addIs,
   1.227 -addEs, addDs etc. Note that claset_of and put_claset allow to manage
   1.228 -clasets separately from the context.
   1.229 +Minor INCOMPATIBILITY.
   1.230  
   1.231  * Simplifier tactics and tools use proper Proof.context instead of
   1.232  historic type simpset.  Old-style declarations like addsimps,
   1.233 @@ -452,9 +440,17 @@
   1.234  old tools by making them depend on (ctxt : Proof.context) instead of
   1.235  (ss : simpset), then turn (simpset_of ctxt) into ctxt.
   1.236  
   1.237 +* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
   1.238 +operate on Proof.context instead of claset, for uniformity with addIs,
   1.239 +addEs, addDs etc. Note that claset_of and put_claset allow to manage
   1.240 +clasets separately from the context.
   1.241 +
   1.242  * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.
   1.243  INCOMPATIBILITY, use @{context} instead.
   1.244  
   1.245 +* Antiquotation @{theory_context A} is similar to @{theory A}, but
   1.246 +presents the result as initial Proof.context.
   1.247 +
   1.248  
   1.249  *** System ***
   1.250  
   1.251 @@ -481,6 +477,13 @@
   1.252  keyword tables): use Isabelle/Scala operations, which inspect outer
   1.253  syntax without requiring to build sessions first.
   1.254  
   1.255 +* Sessions may be organized via 'chapter' specifications in the ROOT
   1.256 +file, which determines a two-level hierarchy of browser info.  The old
   1.257 +tree-like organization via implicit sub-session relation (with its
   1.258 +tendency towards erratic fluctuation of URLs) has been discontinued.
   1.259 +The default chapter is called "Unsorted".  Potential INCOMPATIBILITY
   1.260 +for HTML presentation of theories.
   1.261 +
   1.262  
   1.263  
   1.264  New in Isabelle2013 (February 2013)