--- a/CONTRIBUTORS Sun Sep 18 14:25:53 2011 +0200
+++ b/CONTRIBUTORS Sun Sep 18 14:34:24 2011 +0200
@@ -12,30 +12,30 @@
* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
Refined theory on complete lattices.
+* August 2011: Brian Huffman, Portland State University
+ Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
+
+* June 2011: Brian Huffman, Portland State University
+ Proof method "countable_datatype" for theory Library/Countable.
+
+* 2011: Jasmin Blanchette, TUM
+ Various improvements to Sledgehammer, notably: use of sound
+ translations, support for more provers (Waldmeister, LEO-II,
+ Satallax). Further development of Nitpick and 'try' command.
+
+* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
+ Theory HOL/Library/Cset_Monad allows do notation for computable sets
+ (cset) via the generic monad ad-hoc overloading facility.
+
+* 2011: Johannes Hölzl, Armin Heller, TUM and
+ Bogdan Grechuk, University of Edinburgh
+ Theory HOL/Library/Extended_Reals: real numbers extended with plus
+ and minus infinity.
+
* 2011: Makarius Wenzel, Université Paris-Sud / LRI
Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
Prover IDE.
-* 2011: Jasmin Blanchette, TUM
- Various improvements to Sledgehammer, notably: use of sound translations,
- support for more provers (Waldmeister, LEO-II, Satallax). Further development
- of Nitpick and "try".
-
-* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
- Theory HOL/Library/Cset_Monad allows do notation for computable
- sets (cset) via the generic monad ad-hoc overloading facility.
-
-* 2011: Johannes Hölzl, Armin Heller, TUM,
- and Bogdan Grechuk, University of Edinburgh
- Theory HOL/Library/Extended_Reals: real numbers extended with
- plus and minus infinity.
-
-* June 2011: Brian Huffman, Portland State University
- Proof method 'countable_datatype' for theory Library/Countable.
-
-* August 2011: Brian Huffman, Portland State University
- Misc cleanup of Complex_Main and Multivariate_Analysis.
-
Contributions to Isabelle2011
-----------------------------
--- a/NEWS Sun Sep 18 14:25:53 2011 +0200
+++ b/NEWS Sun Sep 18 14:34:24 2011 +0200
@@ -55,18 +55,6 @@
* Discontinued old lib/scripts/polyml-platform, which has been
obsolete since Isabelle2009-2.
-* Various optional external tools are referenced more robustly and
-uniformly by explicit Isabelle settings as follows:
-
- ISABELLE_CSDP (formerly CSDP_EXE)
- ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH)
- ISABELLE_OCAML (formerly EXEC_OCAML)
- ISABELLE_SWIPL (formerly EXEC_SWIPL)
- ISABELLE_YAP (formerly EXEC_YAP)
-
-Note that automated detection from the file-system or search path has
-been discontinued. INCOMPATIBILITY.
-
* Name space: former unsynchronized references are now proper
configuration options, with more conventional names:
@@ -162,7 +150,8 @@
- Theory Library/Code_Char_ord provides native ordering of
characters in the target language.
- - Commands code_module and code_library are legacy, use export_code instead.
+ - Commands code_module and code_library are legacy, use export_code
+ instead.
- Method "evaluation" is legacy, use method "eval" instead.
@@ -173,8 +162,8 @@
* Declare ext [intro] by default. Rare INCOMPATIBILITY.
-* The misleading name fastsimp has been renamed to fastforce,
- but fastsimp is still available as a legacy feature.
+* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
+still available as a legacy feature for some time.
* Nitpick:
- Added "need" and "total_consts" options.
@@ -184,20 +173,21 @@
* Sledgehammer:
- Use quasi-sound (and efficient) translations by default.
- - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK,
- Waldmeister, and Z3 with TPTP syntax.
- - Automatically preplay and minimize proofs before showing them if this can be
- done within reasonable time.
+ - Added support for the following provers: E-ToFoF, LEO-II,
+ Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.
+ - Automatically preplay and minimize proofs before showing them if
+ this can be done within reasonable time.
- sledgehammer available_provers ~> sledgehammer supported_provers.
INCOMPATIBILITY.
- - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
- and "max_new_mono_instances" options.
- - Removed "explicit_apply" and "full_types" options as well as "Full Types"
- Proof General menu item. INCOMPATIBILITY.
+ - Added "preplay_timeout", "slicing", "type_enc", "sound",
+ "max_mono_iters", and "max_new_mono_instances" options.
+ - Removed "explicit_apply" and "full_types" options as well as "Full
+ Types" Proof General menu item. INCOMPATIBILITY.
* Metis:
- Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
- - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
+ - Obsoleted "metisFT" -- use "metis (full_types)" instead.
+ INCOMPATIBILITY.
* Command 'try':
- Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
@@ -206,23 +196,19 @@
'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
* Quickcheck:
-
- Added "eval" option to evaluate terms for the found counterexample
(currently only supported by the default (exhaustive) tester).
-
- Added post-processing of terms to obtain readable counterexamples
(currently only supported by the default (exhaustive) tester).
-
- New counterexample generator quickcheck[narrowing] enables
narrowing-based testing. Requires the Glasgow Haskell compiler
with its installation location defined in the Isabelle settings
environment as ISABELLE_GHC.
-
- Removed quickcheck tester "SML" based on the SML code generator
(formly in HOL/Library).
-* Function package: discontinued option "tailrec".
-INCOMPATIBILITY. Use 'partial_function' instead.
+* Function package: discontinued option "tailrec". INCOMPATIBILITY,
+use 'partial_function' instead.
* Session HOL-Probability:
- Caratheodory's extension lemma is now proved for ring_of_sets.
@@ -231,9 +217,9 @@
- Use extended reals instead of positive extended
reals. INCOMPATIBILITY.
-* Theory Library/Extended_Reals replaces now the positive extended reals
- found in probability theory. This file is extended by
- Multivariate_Analysis/Extended_Real_Limits.
+* Theory Library/Extended_Reals replaces now the positive extended
+reals found in probability theory. This file is extended by
+Multivariate_Analysis/Extended_Real_Limits.
* Old 'recdef' package has been moved to theory Library/Old_Recdef,
from where it must be imported explicitly. INCOMPATIBILITY.
@@ -241,12 +227,12 @@
* Well-founded recursion combinator "wfrec" has been moved to theory
Library/Wfrec. INCOMPATIBILITY.
-* Theory HOL/Library/Cset_Monad allows do notation for computable
- sets (cset) via the generic monad ad-hoc overloading facility.
+* Theory HOL/Library/Cset_Monad allows do notation for computable sets
+(cset) via the generic monad ad-hoc overloading facility.
* Theories of common data structures are split into theories for
- implementation, an invariant-ensuring type, and connection to
- an abstract type. INCOMPATIBILITY.
+implementation, an invariant-ensuring type, and connection to an
+abstract type. INCOMPATIBILITY.
- RBT is split into RBT and RBT_Mapping.
- AssocList is split and renamed into AList and AList_Mapping.
@@ -423,9 +409,9 @@
bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
-* Theory Complex_Main: The definition of infinite series was generalized.
- Now it is defined on the type class {topological_space, comm_monoid_add}.
- Hence it is useable also for extended real numbers.
+* Theory Complex_Main: The definition of infinite series was
+generalized. Now it is defined on the type class {topological_space,
+comm_monoid_add}. Hence it is useable also for extended real numbers.
* Theory Complex_Main: The complex exponential function "expi" is now
a type-constrained abbreviation for "exp :: complex => complex"; thus
@@ -434,12 +420,6 @@
*** Document preparation ***
-* Localized \isabellestyle switch can be used within blocks or groups
-like this:
-
- \isabellestyle{it} %preferred default
- {\isabellestylett @{text "typewriter stuff"}}
-
* Antiquotation @{rail} layouts railroad syntax diagrams, see also
isar-ref manual, both for description and actual application of the
same.
@@ -454,9 +434,15 @@
* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
-* Discontinued special treatment of hard tabulators, which are better
-avoided in the first place (no universally agreed standard expansion).
-Implicit tab-width is now 1.
+* Localized \isabellestyle switch can be used within blocks or groups
+like this:
+
+ \isabellestyle{it} %preferred default
+ {\isabellestylett @{text "typewriter stuff"}}
+
+* Discontinued special treatment of hard tabulators. Implicit
+tab-width is now defined as 1. Potential INCOMPATIBILITY for visual
+layouts.
*** ML ***
@@ -519,14 +505,26 @@
*** System ***
+* Various optional external tools are referenced more robustly and
+uniformly by explicit Isabelle settings as follows:
+
+ ISABELLE_CSDP (formerly CSDP_EXE)
+ ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH)
+ ISABELLE_OCAML (formerly EXEC_OCAML)
+ ISABELLE_SWIPL (formerly EXEC_SWIPL)
+ ISABELLE_YAP (formerly EXEC_YAP)
+
+Note that automated detection from the file-system or search path has
+been discontinued. INCOMPATIBILITY.
+
* Scala layer provides JVM method invocation service for static
methods of type (String)String, see Invoke_Scala.method in ML. For
example:
Invoke_Scala.method "java.lang.System.getProperty" "java.home"
-Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this
-allows to pass structured values between ML and Scala.
+Together with YXML.string_of_body/parse_body and XML.Encode/Decode
+this allows to pass structured values between ML and Scala.
* The IsabelleText fonts includes some further glyphs to support the
Prover IDE. Potential INCOMPATIBILITY: users who happen to have