Isabelle NEWS -- history user-relevant changes
==============================================
New in this Isabelle version
----------------------------
*** General ***
* Discontinued old form of "escaped symbols" such as \\<forall>. Only
one backslash should be used, even in ML sources.
*** Pure ***
* On instantiation of classes, remaining undefined class parameters
are formally declared. INCOMPATIBILITY.
*** HOL ***
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
etc.
INCOMPATIBILITY.
* New quickcheck implementation using new code generator.
* New type class boolean_algebra.
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
generalized to class semiring_div, subsuming former theorems
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
* Power operations on relations and functions are now one dedicate
constant compow with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
* Implementation of quickcheck using generic code generator; default
generators are provided for all suitable HOL types, records and
datatypes.
* Constants Set.Pow and Set.image now with authentic syntax;
object-logic definitions Set.Pow_def and Set.image_def.
INCOMPATIBILITY.
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
Suc_plus1 -> Suc_eq_plus1
* New sledgehammer option "Full Types" in Proof General settings menu.
Causes full type information to be output to the ATPs. This slows
ATPs down considerably but eliminates a source of unsound "proofs"
that fail later.
* Discontinued ancient tradition to suffix certain ML module names
with "_package", e.g.:
DatatypePackage ~> Datatype
InductivePackage ~> Inductive
etc.
INCOMPATIBILITY.
* NewNumberTheory: Jeremy Avigad's new version of part of
NumberTheory. If possible, use NewNumberTheory, not NumberTheory.
* Simplified interfaces of datatype module. INCOMPATIBILITY.
* Abbreviation "arbitrary" of "undefined" has disappeared; use
"undefined" directly. INCOMPATIBILITY.
* New evaluator "approximate" approximates an real valued term using
the same method as the approximation method.
* Method "approximate" supports now arithmetic expressions as
boundaries of intervals and implements interval splitting and Taylor
series expansion.
* Changed DERIV_intros to a dynamic fact (via Named_Thms). Each of
the theorems in DERIV_intros assumes composition with an additional
function and matches a variable to the derivative, which has to be
solved by the simplifier. Hence (auto intro!: DERIV_intros) computes
the derivative of most elementary terms.
* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
replaced by: (auto intro!: DERIV_intros). INCOMPATIBILITY.
*** ML ***
* Renamed functor TableFun to Table, and GraphFun to Graph. (Since
functors have their own ML name space there is no point to mark them
separately.) Minor INCOMPATIBILITY.
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY.
* Eliminated old Attrib.add_attributes, Method.add_methods and related
cominators for "args". INCOMPATIBILITY, need to use simplified
Attrib/Method.setup introduced in Isabelle2009.
*** System ***
* Discontinued support for Poly/ML 4.x versions.
* Removed "compress" option from isabelle-process and isabelle usedir;
this is always enabled.
New in Isabelle2009 (April 2009)
--------------------------------
*** General ***
* Simplified main Isabelle executables, with less surprises on
case-insensitive file-systems (such as Mac OS).
- The main Isabelle tool wrapper is now called "isabelle" instead of
"isatool."
- The former "isabelle" alias for "isabelle-process" has been
removed (should rarely occur to regular users).
- The former "isabelle-interface" and its alias "Isabelle" have been
removed (interfaces are now regular Isabelle tools).
Within scripts and make files, the Isabelle environment variables
ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
respectively. (The latter are still available as legacy feature.)
The old isabelle-interface wrapper could react in confusing ways if
the interface was uninstalled or changed otherwise. Individual
interface tool configuration is now more explicit, see also the
Isabelle system manual. In particular, Proof General is now available
via "isabelle emacs".
INCOMPATIBILITY, need to adapt derivative scripts. Users may need to
purge installed copies of Isabelle executables and re-run "isabelle
install -p ...", or use symlinks.
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
old ~/isabelle, which was slightly non-standard and apt to cause
surprises on case-insensitive file-systems (such as Mac OS).
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special
care is required when using older releases of Isabelle. Note that
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
Isabelle distribution, in order to use the new ~/.isabelle uniformly.
* Proofs of fully specified statements are run in parallel on
multi-core systems. A speedup factor of 2.5 to 3.2 can be expected on
a regular 4-core machine, if the initial heap space is made reasonably
large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.)
* The main reference manuals ("isar-ref", "implementation", and
"system") have been updated and extended. Formally checked references
as hyperlinks are now available uniformly.
*** Pure ***
* Complete re-implementation of locales. INCOMPATIBILITY in several
respects. The most important changes are listed below. See the
Tutorial on Locales ("locales" manual) for details.
- In locale expressions, instantiation replaces renaming. Parameters
must be declared in a for clause. To aid compatibility with previous
parameter inheritance, in locale declarations, parameters that are not
'touched' (instantiation position "_" or omitted) are implicitly added
with their syntax at the beginning of the for clause.
- Syntax from abbreviations and definitions in locales is available in
locale expressions and context elements. The latter is particularly
useful in locale declarations.
- More flexible mechanisms to qualify names generated by locale
expressions. Qualifiers (prefixes) may be specified in locale
expressions, and can be marked as mandatory (syntax: "name!:") or
optional (syntax "name?:"). The default depends for plain "name:"
depends on the situation where a locale expression is used: in
commands 'locale' and 'sublocale' prefixes are optional, in
'interpretation' and 'interpret' prefixes are mandatory. The old
implicit qualifiers derived from the parameter names of a locale are
no longer generated.
- Command "sublocale l < e" replaces "interpretation l < e". The
instantiation clause in "interpretation" and "interpret" (square
brackets) is no longer available. Use locale expressions.
- When converting proof scripts, mandatory qualifiers in
'interpretation' and 'interpret' should be retained by default, even
if this is an INCOMPATIBILITY compared to former behavior. In the
worst case, use the "name?:" form for non-mandatory ones. Qualifiers
in locale expressions range over a single locale instance only.
- Dropped locale element "includes". This is a major INCOMPATIBILITY.
In existing theorem specifications replace the includes element by the
respective context elements of the included locale, omitting those
that are already present in the theorem specification. Multiple
assume elements of a locale should be replaced by a single one
involving the locale predicate. In the proof body, declarations (most
notably theorems) may be regained by interpreting the respective
locales in the proof context as required (command "interpret").
If using "includes" in replacement of a target solely because the
parameter types in the theorem are not as general as in the target,
consider declaring a new locale with additional type constraints on
the parameters (context element "constrains").
- Discontinued "locale (open)". INCOMPATIBILITY.
- Locale interpretation commands no longer attempt to simplify goal.
INCOMPATIBILITY: in rare situations the generated goal differs. Use
methods intro_locales and unfold_locales to clarify.
- Locale interpretation commands no longer accept interpretation
attributes. INCOMPATIBILITY.
* Class declaration: so-called "base sort" must not be given in import
list any longer, but is inferred from the specification. Particularly
in HOL, write
class foo = ...
instead of
class foo = type + ...
* Class target: global versions of theorems stemming do not carry a
parameter prefix any longer. INCOMPATIBILITY.
* Class 'instance' command no longer accepts attached definitions.
INCOMPATIBILITY, use proper 'instantiation' target instead.
* Recovered hiding of consts, which was accidentally broken in
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really
makes c inaccessible; consider using ``hide (open) const c'' instead.
* Slightly more coherent Pure syntax, with updated documentation in
isar-ref manual. Removed locales meta_term_syntax and
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
INCOMPATIBILITY in rare situations. Note that &&& should not be used
directly in regular applications.
* There is a new syntactic category "float_const" for signed decimal
fractions (e.g. 123.45 or -123.45).
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
interface with 'setup' command instead.
* Command 'local_setup' is similar to 'setup', but operates on a local
theory context.
* The 'axiomatization' command now only works within a global theory
context. INCOMPATIBILITY.
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
hypotheses. Sorts required in the course of reasoning need to be
covered by the constraints in the initial statement, completed by the
type instance information of the background theory. Non-trivial sort
hypotheses, which rarely occur in practice, may be specified via
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example:
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
The result contains an implicit sort hypotheses as before --
SORT_CONSTRAINT premises are eliminated as part of the canonical rule
normalization.
* Generalized Isar history, with support for linear undo, direct state
addressing etc.
* Changed defaults for unify configuration options:
unify_trace_bound = 50 (formerly 25)
unify_search_bound = 60 (formerly 30)
* Different bookkeeping for code equations (INCOMPATIBILITY):
a) On theory merge, the last set of code equations for a particular
constant is taken (in accordance with the policy applied by other
parts of the code generator framework).
b) Code equations stemming from explicit declarations (e.g. code
attribute) gain priority over default code equations stemming
from definition, primrec, fun etc.
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
* Unified theorem tables for both code generators. Thus [code
func] has disappeared and only [code] remains. INCOMPATIBILITY.
* Command 'find_consts' searches for constants based on type and name
patterns, e.g.
find_consts "_ => bool"
By default, matching is against subtypes, but it may be restricted to
the whole type. Searching by name is possible. Multiple queries are
conjunctive and queries may be negated by prefixing them with a
hyphen:
find_consts strict: "_ => bool" name: "Int" -"int => int"
* New 'find_theorems' criterion "solves" matches theorems that
directly solve the current goal (modulo higher-order unification).
* Auto solve feature for main theorem statements: whenever a new goal
is stated, "find_theorems solves" is called; any theorems that could
solve the lemma directly are listed as part of the goal state.
Cf. associated options in Proof General Isabelle settings menu,
enabled by default, with reasonable timeout for pathological cases of
higher-order unification.
*** Document preparation ***
* Antiquotation @{lemma} now imitates a regular terminal proof,
demanding keyword 'by' and supporting the full method expression
syntax just like the Isar command 'by'.
*** HOL ***
* Integrated main parts of former image HOL-Complex with HOL. Entry
points Main and Complex_Main remain as before.
* Logic image HOL-Plain provides a minimal HOL with the most important