misc tuning for release;
authorwenzelm
Sun Sep 18 14:34:24 2011 +0200 (2011-09-18)
changeset 44967b94c1614e7d5
parent 44966 1db165e0bd97
child 44968 52744e144432
misc tuning for release;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Sun Sep 18 14:25:53 2011 +0200
     1.2 +++ b/CONTRIBUTORS	Sun Sep 18 14:34:24 2011 +0200
     1.3 @@ -12,30 +12,30 @@
     1.4  * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
     1.5    Refined theory on complete lattices.
     1.6  
     1.7 +* August 2011: Brian Huffman, Portland State University
     1.8 +  Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
     1.9 +
    1.10 +* June 2011: Brian Huffman, Portland State University
    1.11 +  Proof method "countable_datatype" for theory Library/Countable.
    1.12 +
    1.13 +* 2011: Jasmin Blanchette, TUM
    1.14 +  Various improvements to Sledgehammer, notably: use of sound
    1.15 +  translations, support for more provers (Waldmeister, LEO-II,
    1.16 +  Satallax). Further development of Nitpick and 'try' command.
    1.17 +
    1.18 +* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
    1.19 +  Theory HOL/Library/Cset_Monad allows do notation for computable sets
    1.20 +  (cset) via the generic monad ad-hoc overloading facility.
    1.21 +
    1.22 +* 2011: Johannes Hölzl, Armin Heller, TUM and
    1.23 +  Bogdan Grechuk, University of Edinburgh
    1.24 +  Theory HOL/Library/Extended_Reals: real numbers extended with plus
    1.25 +  and minus infinity.
    1.26 +
    1.27  * 2011: Makarius Wenzel, Université Paris-Sud / LRI
    1.28    Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
    1.29    Prover IDE.
    1.30  
    1.31 -* 2011: Jasmin Blanchette, TUM
    1.32 -  Various improvements to Sledgehammer, notably: use of sound translations,
    1.33 -  support for more provers (Waldmeister, LEO-II, Satallax). Further development
    1.34 -  of Nitpick and "try".
    1.35 -
    1.36 -* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
    1.37 -  Theory HOL/Library/Cset_Monad allows do notation for computable
    1.38 -  sets (cset) via the generic monad ad-hoc overloading facility.
    1.39 -
    1.40 -* 2011: Johannes Hölzl, Armin Heller, TUM,
    1.41 -  and Bogdan Grechuk, University of Edinburgh
    1.42 -  Theory HOL/Library/Extended_Reals: real numbers extended with
    1.43 -  plus and minus infinity.
    1.44 -
    1.45 -* June 2011: Brian Huffman, Portland State University
    1.46 -  Proof method 'countable_datatype' for theory Library/Countable.
    1.47 -
    1.48 -* August 2011: Brian Huffman, Portland State University
    1.49 -  Misc cleanup of Complex_Main and Multivariate_Analysis.
    1.50 -
    1.51  
    1.52  Contributions to Isabelle2011
    1.53  -----------------------------
     2.1 --- a/NEWS	Sun Sep 18 14:25:53 2011 +0200
     2.2 +++ b/NEWS	Sun Sep 18 14:34:24 2011 +0200
     2.3 @@ -55,18 +55,6 @@
     2.4  * Discontinued old lib/scripts/polyml-platform, which has been
     2.5  obsolete since Isabelle2009-2.
     2.6  
     2.7 -* Various optional external tools are referenced more robustly and
     2.8 -uniformly by explicit Isabelle settings as follows:
     2.9 -
    2.10 -  ISABELLE_CSDP   (formerly CSDP_EXE)
    2.11 -  ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)
    2.12 -  ISABELLE_OCAML  (formerly EXEC_OCAML)
    2.13 -  ISABELLE_SWIPL  (formerly EXEC_SWIPL)
    2.14 -  ISABELLE_YAP    (formerly EXEC_YAP)
    2.15 -
    2.16 -Note that automated detection from the file-system or search path has
    2.17 -been discontinued.  INCOMPATIBILITY.
    2.18 -
    2.19  * Name space: former unsynchronized references are now proper
    2.20  configuration options, with more conventional names:
    2.21  
    2.22 @@ -162,7 +150,8 @@
    2.23    - Theory Library/Code_Char_ord provides native ordering of
    2.24      characters in the target language.
    2.25  
    2.26 -  - Commands code_module and code_library are legacy, use export_code instead.
    2.27 +  - Commands code_module and code_library are legacy, use export_code
    2.28 +    instead.
    2.29  
    2.30    - Method "evaluation" is legacy, use method "eval" instead.
    2.31  
    2.32 @@ -173,8 +162,8 @@
    2.33  
    2.34  * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
    2.35  
    2.36 -* The misleading name fastsimp has been renamed to fastforce,
    2.37 -  but fastsimp is still available as a legacy feature.
    2.38 +* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
    2.39 +still available as a legacy feature for some time.
    2.40  
    2.41  * Nitpick:
    2.42    - Added "need" and "total_consts" options.
    2.43 @@ -184,20 +173,21 @@
    2.44  
    2.45  * Sledgehammer:
    2.46    - Use quasi-sound (and efficient) translations by default.
    2.47 -  - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK,
    2.48 -    Waldmeister, and Z3 with TPTP syntax.
    2.49 -  - Automatically preplay and minimize proofs before showing them if this can be
    2.50 -    done within reasonable time.
    2.51 +  - Added support for the following provers: E-ToFoF, LEO-II,
    2.52 +    Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.
    2.53 +  - Automatically preplay and minimize proofs before showing them if
    2.54 +    this can be done within reasonable time.
    2.55    - sledgehammer available_provers ~> sledgehammer supported_provers.
    2.56      INCOMPATIBILITY.
    2.57 -  - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
    2.58 -    and "max_new_mono_instances" options.
    2.59 -  - Removed "explicit_apply" and "full_types" options as well as "Full Types"
    2.60 -    Proof General menu item. INCOMPATIBILITY.
    2.61 +  - Added "preplay_timeout", "slicing", "type_enc", "sound",
    2.62 +    "max_mono_iters", and "max_new_mono_instances" options.
    2.63 +  - Removed "explicit_apply" and "full_types" options as well as "Full
    2.64 +    Types" Proof General menu item. INCOMPATIBILITY.
    2.65  
    2.66  * Metis:
    2.67    - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
    2.68 -  - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
    2.69 +  - Obsoleted "metisFT" -- use "metis (full_types)" instead.
    2.70 +    INCOMPATIBILITY.
    2.71  
    2.72  * Command 'try':
    2.73    - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
    2.74 @@ -206,23 +196,19 @@
    2.75      'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
    2.76  
    2.77  * Quickcheck:
    2.78 -
    2.79    - Added "eval" option to evaluate terms for the found counterexample
    2.80      (currently only supported by the default (exhaustive) tester).
    2.81 -
    2.82    - Added post-processing of terms to obtain readable counterexamples
    2.83      (currently only supported by the default (exhaustive) tester).
    2.84 -
    2.85    - New counterexample generator quickcheck[narrowing] enables
    2.86      narrowing-based testing.  Requires the Glasgow Haskell compiler
    2.87      with its installation location defined in the Isabelle settings
    2.88      environment as ISABELLE_GHC.
    2.89 -
    2.90    - Removed quickcheck tester "SML" based on the SML code generator
    2.91      (formly in HOL/Library).
    2.92  
    2.93 -* Function package: discontinued option "tailrec".
    2.94 -INCOMPATIBILITY. Use 'partial_function' instead.
    2.95 +* Function package: discontinued option "tailrec".  INCOMPATIBILITY,
    2.96 +use 'partial_function' instead.
    2.97  
    2.98  * Session HOL-Probability:
    2.99    - Caratheodory's extension lemma is now proved for ring_of_sets.
   2.100 @@ -231,9 +217,9 @@
   2.101    - Use extended reals instead of positive extended
   2.102      reals. INCOMPATIBILITY.
   2.103  
   2.104 -* Theory Library/Extended_Reals replaces now the positive extended reals
   2.105 -  found in probability theory. This file is extended by
   2.106 -  Multivariate_Analysis/Extended_Real_Limits.
   2.107 +* Theory Library/Extended_Reals replaces now the positive extended
   2.108 +reals found in probability theory. This file is extended by
   2.109 +Multivariate_Analysis/Extended_Real_Limits.
   2.110  
   2.111  * Old 'recdef' package has been moved to theory Library/Old_Recdef,
   2.112  from where it must be imported explicitly.  INCOMPATIBILITY.
   2.113 @@ -241,12 +227,12 @@
   2.114  * Well-founded recursion combinator "wfrec" has been moved to theory
   2.115  Library/Wfrec. INCOMPATIBILITY.
   2.116  
   2.117 -* Theory HOL/Library/Cset_Monad allows do notation for computable
   2.118 -  sets (cset) via the generic monad ad-hoc overloading facility.
   2.119 +* Theory HOL/Library/Cset_Monad allows do notation for computable sets
   2.120 +(cset) via the generic monad ad-hoc overloading facility.
   2.121  
   2.122  * Theories of common data structures are split into theories for
   2.123 -  implementation, an invariant-ensuring type, and connection to
   2.124 -  an abstract type. INCOMPATIBILITY.
   2.125 +implementation, an invariant-ensuring type, and connection to an
   2.126 +abstract type. INCOMPATIBILITY.
   2.127  
   2.128    - RBT is split into RBT and RBT_Mapping.
   2.129    - AssocList is split and renamed into AList and AList_Mapping.
   2.130 @@ -423,9 +409,9 @@
   2.131    bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
   2.132    LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
   2.133  
   2.134 -* Theory Complex_Main: The definition of infinite series was generalized.
   2.135 -  Now it is defined on the type class {topological_space, comm_monoid_add}.
   2.136 -  Hence it is useable also for extended real numbers.
   2.137 +* Theory Complex_Main: The definition of infinite series was
   2.138 +generalized.  Now it is defined on the type class {topological_space,
   2.139 +comm_monoid_add}.  Hence it is useable also for extended real numbers.
   2.140  
   2.141  * Theory Complex_Main: The complex exponential function "expi" is now
   2.142  a type-constrained abbreviation for "exp :: complex => complex"; thus
   2.143 @@ -434,12 +420,6 @@
   2.144  
   2.145  *** Document preparation ***
   2.146  
   2.147 -* Localized \isabellestyle switch can be used within blocks or groups
   2.148 -like this:
   2.149 -
   2.150 -  \isabellestyle{it}  %preferred default
   2.151 -  {\isabellestylett @{text "typewriter stuff"}}
   2.152 -
   2.153  * Antiquotation @{rail} layouts railroad syntax diagrams, see also
   2.154  isar-ref manual, both for description and actual application of the
   2.155  same.
   2.156 @@ -454,9 +434,15 @@
   2.157  * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
   2.158  (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
   2.159  
   2.160 -* Discontinued special treatment of hard tabulators, which are better
   2.161 -avoided in the first place (no universally agreed standard expansion).
   2.162 -Implicit tab-width is now 1.
   2.163 +* Localized \isabellestyle switch can be used within blocks or groups
   2.164 +like this:
   2.165 +
   2.166 +  \isabellestyle{it}  %preferred default
   2.167 +  {\isabellestylett @{text "typewriter stuff"}}
   2.168 +
   2.169 +* Discontinued special treatment of hard tabulators.  Implicit
   2.170 +tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual
   2.171 +layouts.
   2.172  
   2.173  
   2.174  *** ML ***
   2.175 @@ -519,14 +505,26 @@
   2.176  
   2.177  *** System ***
   2.178  
   2.179 +* Various optional external tools are referenced more robustly and
   2.180 +uniformly by explicit Isabelle settings as follows:
   2.181 +
   2.182 +  ISABELLE_CSDP   (formerly CSDP_EXE)
   2.183 +  ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)
   2.184 +  ISABELLE_OCAML  (formerly EXEC_OCAML)
   2.185 +  ISABELLE_SWIPL  (formerly EXEC_SWIPL)
   2.186 +  ISABELLE_YAP    (formerly EXEC_YAP)
   2.187 +
   2.188 +Note that automated detection from the file-system or search path has
   2.189 +been discontinued.  INCOMPATIBILITY.
   2.190 +
   2.191  * Scala layer provides JVM method invocation service for static
   2.192  methods of type (String)String, see Invoke_Scala.method in ML.  For
   2.193  example:
   2.194  
   2.195    Invoke_Scala.method "java.lang.System.getProperty" "java.home"
   2.196  
   2.197 -Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this
   2.198 -allows to pass structured values between ML and Scala.
   2.199 +Together with YXML.string_of_body/parse_body and XML.Encode/Decode
   2.200 +this allows to pass structured values between ML and Scala.
   2.201  
   2.202  * The IsabelleText fonts includes some further glyphs to support the
   2.203  Prover IDE.  Potential INCOMPATIBILITY: users who happen to have