Isabelle NEWS -- history user-relevant changes

==============================================

New in this Isabelle version

----------------------------

*** General ***

* Parallelization of nested Isar proofs is subject to

Goal.parallel_proofs_threshold (default 100).  See also isabelle

usedir option -Q.

* Discontinued support for Poly/ML 5.2, which was the last version

without proper multithreading and TimeLimit implementation.

* Discontinued old lib/scripts/polyml-platform, which has been

obsolete since Isabelle2009-2.

*** HOL ***

* Nitpick:

  - Renamed attribute: nitpick_def ~> nitpick_unfold.

    INCOMPATIBILITY.

* Sledgehammer:

  - sledgehammer available_provers ~> sledgehammer supported_provers

    INCOMPATIBILITY.

*** Document preparation ***

* New term style "isub" as ad-hoc conversion of variables x1, y23 into

subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.

New in Isabelle2011 (January 2011)

----------------------------------

*** General ***

* Experimental Prover IDE based on Isabelle/Scala and jEdit (see

src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with

useful tooltips and hyperlinks produced from its static analysis.  The

bundled component provides an executable Isabelle tool that can be run

like this:

  Isabelle2011/bin/isabelle jedit

* Significantly improved Isabelle/Isar implementation manual.

* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

(and thus refers to something like $HOME/.isabelle/Isabelle2011),

while the default heap location within that directory lacks that extra

suffix.  This isolates multiple Isabelle installations from each

other, avoiding problems with old settings in new versions.

INCOMPATIBILITY, need to copy/upgrade old user settings manually.

* Source files are always encoded as UTF-8, instead of old-fashioned

ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require

the following package declarations:

  \usepackage[utf8]{inputenc}

  \usepackage{textcomp}

* Explicit treatment of UTF-8 sequences as Isabelle symbols, such that

a Unicode character is treated as a single symbol, not a sequence of

non-ASCII bytes as before.  Since Isabelle/ML string literals may

contain symbols without further backslash escapes, Unicode can now be

used here as well.  Recall that Symbol.explode in ML provides a

consistent view on symbols, while raw explode (or String.explode)

merely give a byte-oriented representation.

* Theory loader: source files are primarily located via the master

directory of each theory node (where the .thy file itself resides).

The global load path is still partially available as legacy feature.

Minor INCOMPATIBILITY due to subtle change in file lookup: use

explicit paths, relatively to the theory.

* Special treatment of ML file names has been discontinued.

Historically, optional extensions .ML or .sml were added on demand --

at the cost of clarity of file dependencies.  Recall that Isabelle/ML

files exclusively use the .ML extension.  Minor INCOMPATIBILTY.

* Various options that affect pretty printing etc. are now properly

handled within the context via configuration options, instead of

unsynchronized references or print modes.  There are both ML Config.T

entities and Isar declaration attributes to access these.

  ML (Config.T)                 Isar (attribute)

  eta_contract                  eta_contract

  show_brackets                 show_brackets

  show_sorts                    show_sorts

  show_types                    show_types

  show_question_marks           show_question_marks

  show_consts                   show_consts

  show_abbrevs                  show_abbrevs

  Syntax.ast_trace              syntax_ast_trace

  Syntax.ast_stat               syntax_ast_stat

  Syntax.ambiguity_level        syntax_ambiguity_level

  Goal_Display.goals_limit      goals_limit

  Goal_Display.show_main_goal   show_main_goal

  Method.rule_trace             rule_trace

  Thy_Output.display            thy_output_display

  Thy_Output.quotes             thy_output_quotes

  Thy_Output.indent             thy_output_indent

  Thy_Output.source             thy_output_source

  Thy_Output.break              thy_output_break

Note that corresponding "..._default" references in ML may only be

changed globally at the ROOT session setup, but *not* within a theory.

The option "show_abbrevs" supersedes the former print mode

"no_abbrevs" with inverted meaning.

* More systematic naming of some configuration options.

INCOMPATIBILITY.

  trace_simp  ~>  simp_trace

  debug_simp  ~>  simp_debug

* Support for real valued configuration options, using simplistic

floating-point notation that coincides with the inner syntax for

float_token.

* Support for real valued preferences (with approximative PGIP type):

front-ends need to accept "pgint" values in float notation.

INCOMPATIBILITY.

* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from

DejaVu Sans.

* Discontinued support for Poly/ML 5.0 and 5.1 versions.

*** Pure ***

* Command 'type_synonym' (with single argument) replaces somewhat

outdated 'types', which is still available as legacy feature for some

time.

* Command 'nonterminal' (with 'and' separated list of arguments)

replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.

* Command 'notepad' replaces former 'example_proof' for

experimentation in Isar without any result.  INCOMPATIBILITY.

* Locale interpretation commands 'interpret' and 'sublocale' accept

lists of equations to map definitions in a locale to appropriate

entities in the context of the interpretation.  The 'interpretation'

command already provided this functionality.

* Diagnostic command 'print_dependencies' prints the locale instances

that would be activated if the specified expression was interpreted in

the current context.  Variant "print_dependencies!" assumes a context

without interpretations.

* Diagnostic command 'print_interps' prints interpretations in proofs

in addition to interpretations in theories.

* Discontinued obsolete 'global' and 'local' commands to manipulate

the theory name space.  Rare INCOMPATIBILITY.  The ML functions

Sign.root_path and Sign.local_path may be applied directly where this

feature is still required for historical reasons.

* Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use

'definition' instead.

* The "prems" fact, which refers to the accidental collection of

foundational premises in the context, is now explicitly marked as

legacy feature and will be discontinued soon.  Consider using "assms"

of the head statement or reference facts by explicit names.

* Document antiquotations @{class} and @{type} print classes and type

constructors.

* Document antiquotation @{file} checks file/directory entries within

the local file system.

*** HOL ***

* Coercive subtyping: functions can be declared as coercions and type

inference will add them as necessary upon input of a term.  Theory

Complex_Main declares real :: nat => real and real :: int => real as

coercions. A coercion function f is declared like this:

  declare [[coercion f]]

To lift coercions through type constructors (e.g. from nat => real to

nat list => real list), map functions can be declared, e.g.

  declare [[coercion_map map]]

Currently coercion inference is activated only in theories including

real numbers, i.e. descendants of Complex_Main.  This is controlled by

the configuration option "coercion_enabled", e.g. it can be enabled in

other theories like this:

  declare [[coercion_enabled]]

* Command 'partial_function' provides basic support for recursive

function definitions over complete partial orders.  Concrete instances

are provided for i) the option type, ii) tail recursion on arbitrary

types, and iii) the heap monad of Imperative_HOL.  See

src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy

for examples.

* Function package: f.psimps rules are no longer implicitly declared

as [simp].  INCOMPATIBILITY.

* Datatype package: theorems generated for executable equality (class

"eq") carry proper names and are treated as default code equations.

* Inductive package: now offers command 'inductive_simps' to

automatically derive instantiated and simplified equations for

inductive predicates, similar to 'inductive_cases'.

* Command 'enriched_type' allows to register properties of the

functorial structure of types.

* Improved infrastructure for term evaluation using code generator

techniques, in particular static evaluation conversions.

* Code generator: Scala (2.8 or higher) has been added to the target

languages.

* Code generator: globbing constant expressions "*" and "Theory.*"

have been replaced by the more idiomatic "_" and "Theory._".

INCOMPATIBILITY.

* Code generator: export_code without explicit file declaration prints

to standard output.  INCOMPATIBILITY.

* Code generator: do not print function definitions for case

combinators any longer.

* Code generator: simplification with rules determined with

src/Tools/Code/code_simp.ML and method "code_simp".

* Code generator for records: more idiomatic representation of record

types.  Warning: records are not covered by ancient SML code

generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable

rep_datatype declaration helps to succeed then:

  record 'a foo = ...

  ...

  rep_datatype foo_ext ...

* Records: logical foundation type for records does not carry a

'_type' suffix any longer (obsolete due to authentic syntax).

INCOMPATIBILITY.

* Quickcheck now by default uses exhaustive testing instead of random

testing.  Random testing can be invoked by "quickcheck [random]",

exhaustive testing by "quickcheck [exhaustive]".

* Quickcheck instantiates polymorphic types with small finite

datatypes by default. This enables a simple execution mechanism to

handle quantifiers and function equality over the finite datatypes.

* Quickcheck random generator has been renamed from "code" to

"random".  INCOMPATIBILITY.

* Quickcheck now has a configurable time limit which is set to 30

seconds by default. This can be changed by adding [timeout = n] to the

quickcheck command. The time limit for Auto Quickcheck is still set

independently.

* Quickcheck in locales considers interpretations of that locale for

counter example search.

* Sledgehammer:

  - Added "smt" and "remote_smt" provers based on the "smt" proof

    method. See the Sledgehammer manual for details ("isabelle doc

    sledgehammer").

  - Renamed commands:

    sledgehammer atp_info ~> sledgehammer running_provers

    sledgehammer atp_kill ~> sledgehammer kill_provers

    sledgehammer available_atps ~> sledgehammer available_provers

    INCOMPATIBILITY.

  - Renamed options:

    sledgehammer [atps = ...] ~> sledgehammer [provers = ...]

    sledgehammer [atp = ...] ~> sledgehammer [prover = ...]

    sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]

    (and "ms" and "min" are no longer supported)

    INCOMPATIBILITY.

* Nitpick:

  - Renamed options:

    nitpick [timeout = 77 s] ~> nitpick [timeout = 77]

    nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]

    INCOMPATIBILITY.

  - Added support for partial quotient types.

  - Added local versions of the "Nitpick.register_xxx" functions.

  - Added "whack" option.

  - Allow registration of quotient types as codatatypes.

  - Improved "merge_type_vars" option to merge more types.

  - Removed unsound "fast_descrs" option.

  - Added custom symmetry breaking for datatypes, making it possible to reach

    higher cardinalities.

  - Prevent the expansion of too large definitions.

* Proof methods "metis" and "meson" now have configuration options

"meson_trace", "metis_trace", and "metis_verbose" that can be enabled

to diagnose these tools. E.g.

    using [[metis_trace = true]]

* Auto Solve: Renamed "Auto Solve Direct".  The tool is now available

manually as command 'solve_direct'.

* The default SMT solver Z3 must be enabled explicitly (due to

licensing issues) by setting the environment variable

Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For

commercial applications, the SMT solver CVC3 is provided as fall-back;

changing the SMT solver is done via the configuration option

"smt_solver".

* Remote SMT solvers need to be referred to by the "remote_" prefix,

i.e. "remote_cvc3" and "remote_z3".

* Added basic SMT support for datatypes, records, and typedefs using

the oracle mode (no proofs).  Direct support of pairs has been dropped

in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT

support for a similar behavior).  Minor INCOMPATIBILITY.

* Changed SMT configuration options:

  - Renamed:

    z3_proofs ~> smt_oracle (with inverted meaning)

    z3_trace_assms ~> smt_trace_used_facts

    INCOMPATIBILITY.

  - Added:

    smt_verbose

    smt_random_seed

    smt_datatypes

    smt_infer_triggers

    smt_monomorph_limit

    cvc3_options

    remote_cvc3_options

    remote_z3_options

    yices_options

* Boogie output files (.b2i files) need to be declared in the theory

header.

* Simplification procedure "list_to_set_comprehension" rewrites list

comprehensions applied to List.set to set comprehensions.  Occasional

INCOMPATIBILITY, may be deactivated like this:

  declare [[simproc del: list_to_set_comprehension]]

* Removed old version of primrec package.  INCOMPATIBILITY.

* Removed simplifier congruence rule of "prod_case", as has for long

been the case with "split".  INCOMPATIBILITY.

* String.literal is a type, but not a datatype.  INCOMPATIBILITY.

* Removed [split_format ... and ... and ...] version of

[split_format].  Potential INCOMPATIBILITY.

* Predicate "sorted" now defined inductively, with nice induction

rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.

* Constant "contents" renamed to "the_elem", to free the generic name

contents for other uses.  INCOMPATIBILITY.

* Renamed class eq and constant eq (for code generation) to class

equal and constant equal, plus renaming of related facts and various

tuning.  INCOMPATIBILITY.

* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

* Removed output syntax "'a ~=> 'b" for "'a => 'b option".

INCOMPATIBILITY.

* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to

avoid confusion with finite sets.  INCOMPATIBILITY.

* Abandoned locales equiv, congruent and congruent2 for equivalence

relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same

for congruent(2)).

* Some previously unqualified names have been qualified:

  types

    bool ~> HOL.bool

    nat ~> Nat.nat

  constants

    Trueprop ~> HOL.Trueprop

    True ~> HOL.True

    False ~> HOL.False

    op & ~> HOL.conj

    op | ~> HOL.disj

    op --> ~> HOL.implies

    op = ~> HOL.eq

    Not ~> HOL.Not

    The ~> HOL.The

    All ~> HOL.All

    Ex ~> HOL.Ex

    Ex1 ~> HOL.Ex1

    Let ~> HOL.Let

    If ~> HOL.If

    Ball ~> Set.Ball

    Bex ~> Set.Bex

    Suc ~> Nat.Suc

    Pair ~> Product_Type.Pair

    fst ~> Product_Type.fst

    snd ~> Product_Type.snd

    curry ~> Product_Type.curry

    op : ~> Set.member

    Collect ~> Set.Collect

INCOMPATIBILITY.

* More canonical naming convention for some fundamental definitions:

    bot_bool_eq ~> bot_bool_def

    top_bool_eq ~> top_bool_def

    inf_bool_eq ~> inf_bool_def

    sup_bool_eq ~> sup_bool_def

    bot_fun_eq  ~> bot_fun_def

    top_fun_eq  ~> top_fun_def

    inf_fun_eq  ~> inf_fun_def

    sup_fun_eq  ~> sup_fun_def

INCOMPATIBILITY.

* More stylized fact names:

  expand_fun_eq ~> fun_eq_iff

  expand_set_eq ~> set_eq_iff

  set_ext       ~> set_eqI

  nat_number    ~> eval_nat_numeral

INCOMPATIBILITY.

* Refactoring of code-generation specific operations in theory List:

  constants

    null ~> List.null

  facts

    mem_iff ~> member_def

    null_empty ~> null_def

INCOMPATIBILITY.  Note that these were not supposed to be used

regularly unless for striking reasons; their main purpose was code

generation.

Various operations from the Haskell prelude are used for generating

Haskell code.

* Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV".  Term

"surj f" is now an abbreviation of "range f = UNIV".  The theorems

bij_def and surj_def are unchanged.  INCOMPATIBILITY.

* Abolished some non-alphabetic type names: "prod" and "sum" replace

"*" and "+" respectively.  INCOMPATIBILITY.

* Name "Plus" of disjoint sum operator "<+>" is now hidden.  Write

"Sum_Type.Plus" instead.

* Constant "split" has been merged with constant "prod_case"; names of

ML functions, facts etc. involving split have been retained so far,

though.  INCOMPATIBILITY.

* Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"

instead.  INCOMPATIBILITY.

* Removed lemma "Option.is_none_none" which duplicates "is_none_def".

INCOMPATIBILITY.

* Former theory Library/Enum is now part of the HOL-Main image.

INCOMPATIBILITY: all constants of the Enum theory now have to be

referred to by its qualified name.

  enum    ~>  Enum.enum

  nlists  ~>  Enum.nlists

  product ~>  Enum.product

* Theory Library/Monad_Syntax provides do-syntax for monad types.

Syntax in Library/State_Monad has been changed to avoid ambiguities.

INCOMPATIBILITY.

* Theory Library/SetsAndFunctions has been split into

Library/Function_Algebras and Library/Set_Algebras; canonical names

for instance definitions for functions; various improvements.

INCOMPATIBILITY.

* Theory Library/Multiset provides stable quicksort implementation of

sort_key.

* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.

INCOMPATIBILITY.

* Session Multivariate_Analysis: introduced a type class for euclidean

space.  Most theorems are now stated in terms of euclidean spaces

instead of finite cartesian products.

  types

    real ^ 'n ~>  'a::real_vector

              ~>  'a::euclidean_space

              ~>  'a::ordered_euclidean_space

        (depends on your needs)

  constants

     _ $ _        ~> _ $$ _

     \<chi> x. _  ~> \<chi>\<chi> x. _

     CARD('n)     ~> DIM('a)

Also note that the indices are now natural numbers and not from some

finite type. Finite cartesian products of euclidean spaces, products

of euclidean spaces the real and complex numbers are instantiated to

be euclidean_spaces.  INCOMPATIBILITY.

* Session Probability: introduced pextreal as positive extended real

numbers.  Use pextreal as value for measures.  Introduce the

Radon-Nikodym derivative, product spaces and Fubini's theorem for

arbitrary sigma finite measures.  Introduces Lebesgue measure based on

the integral in Multivariate Analysis.  INCOMPATIBILITY.

* Session Imperative_HOL: revamped, corrected dozens of inadequacies.

INCOMPATIBILITY.

* Session SPARK (with image HOL-SPARK) provides commands to load and

prove verification conditions generated by the SPARK Ada program

verifier.  See also src/HOL/SPARK and src/HOL/SPARK/Examples.

*** HOL-Algebra ***

* Theorems for additive ring operations (locale abelian_monoid and

descendants) are generated by interpretation from their multiplicative

counterparts.  Names (in particular theorem names) have the mandatory

qualifier 'add'.  Previous theorem names are redeclared for

compatibility.

* Structure "int_ring" is now an abbreviation (previously a

definition).  This fits more natural with advanced interpretations.

*** HOLCF ***

* The domain package now runs in definitional mode by default: The

former command 'new_domain' is now called 'domain'.  To use the domain

package in its original axiomatic mode, use 'domain (unsafe)'.

INCOMPATIBILITY.

* The new class "domain" is now the default sort.  Class "predomain"

is an unpointed version of "domain". Theories can be updated by

replacing sort annotations as shown below.  INCOMPATIBILITY.

  'a::type ~> 'a::countable

  'a::cpo  ~> 'a::predomain

  'a::pcpo ~> 'a::domain

* The old type class "rep" has been superseded by class "domain".

Accordingly, users of the definitional package must remove any

"default_sort rep" declarations.  INCOMPATIBILITY.

* The domain package (definitional mode) now supports unpointed

predomain argument types, as long as they are marked 'lazy'. (Strict

arguments must be in class "domain".) For example, the following

domain definition now works:

  domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")

* Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class

instances for types from main HOL: bool, nat, int, char, 'a + 'b,

'a option, and 'a list.  Additionally, it configures fixrec and the

domain package to work with these types.  For example:

  fixrec isInl :: "('a + 'b) u -> tr"

    where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"

  domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")

* The "(permissive)" option of fixrec has been replaced with a

per-equation "(unchecked)" option. See

src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.

* The "bifinite" class no longer fixes a constant "approx"; the class

now just asserts that such a function exists.  INCOMPATIBILITY.

* Former type "alg_defl" has been renamed to "defl".  HOLCF no longer

defines an embedding of type 'a defl into udom by default; instances

of "bifinite" and "domain" classes are available in

src/HOL/HOLCF/Library/Defl_Bifinite.thy.

* The syntax "REP('a)" has been replaced with "DEFL('a)".

* The predicate "directed" has been removed.  INCOMPATIBILITY.

* The type class "finite_po" has been removed.  INCOMPATIBILITY.

* The function "cprod_map" has been renamed to "prod_map".

INCOMPATIBILITY.

* The monadic bind operator on each powerdomain has new binder syntax

similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents

"upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".

* The infix syntax for binary union on each powerdomain has changed

from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set

syntax.  INCOMPATIBILITY.

* The constant "UU" has been renamed to "bottom".  The syntax "UU" is

still supported as an input translation.

* Renamed some theorems (the original names are also still available).

  expand_fun_below   ~> fun_below_iff

  below_fun_ext      ~> fun_belowI

  expand_cfun_eq     ~> cfun_eq_iff

  ext_cfun           ~> cfun_eqI

  expand_cfun_below  ~> cfun_below_iff

  below_cfun_ext     ~> cfun_belowI

  cont2cont_Rep_CFun ~> cont2cont_APP

* The Abs and Rep functions for various types have changed names.

Related theorem names have also changed to match. INCOMPATIBILITY.

  Rep_CFun  ~> Rep_cfun

  Abs_CFun  ~> Abs_cfun

  Rep_Sprod ~> Rep_sprod

  Abs_Sprod ~> Abs_sprod

  Rep_Ssum  ~> Rep_ssum

  Abs_Ssum  ~> Abs_ssum

* Lemmas with names of the form *_defined_iff or *_strict_iff have

been renamed to *_bottom_iff.  INCOMPATIBILITY.

* Various changes to bisimulation/coinduction with domain package:

  - Definitions of "bisim" constants no longer mention definedness.

  - With mutual recursion, "bisim" predicate is now curried.

  - With mutual recursion, each type gets a separate coind theorem.

  - Variable names in bisim_def and coinduct rules have changed.

INCOMPATIBILITY.

* Case combinators generated by the domain package for type "foo" are

now named "foo_case" instead of "foo_when".  INCOMPATIBILITY.

* Several theorems have been renamed to more accurately reflect the

names of constants and types involved.  INCOMPATIBILITY.

  thelub_const    ~> lub_const

  lub_const       ~> is_lub_const

  thelubI         ~> lub_eqI

  is_lub_lub      ~> is_lubD2

  lubI            ~> is_lub_lub

  unique_lub      ~> is_lub_unique

  is_ub_lub       ~> is_lub_rangeD1

  lub_bin_chain   ~> is_lub_bin_chain

  lub_fun         ~> is_lub_fun

  thelub_fun      ~> lub_fun

  thelub_cfun     ~> lub_cfun

  thelub_Pair     ~> lub_Pair

  lub_cprod       ~> is_lub_prod

  thelub_cprod    ~> lub_prod

  minimal_cprod   ~> minimal_prod

  inst_cprod_pcpo ~> inst_prod_pcpo

  UU_I            ~> bottomI

  compact_UU      ~> compact_bottom

  deflation_UU    ~> deflation_bottom

  finite_deflation_UU ~> finite_deflation_bottom

* Many legacy theorem names have been discontinued.  INCOMPATIBILITY.

  sq_ord_less_eq_trans ~> below_eq_trans

  sq_ord_eq_less_trans ~> eq_below_trans

  refl_less            ~> below_refl

  trans_less           ~> below_trans

  antisym_less         ~> below_antisym

  antisym_less_inverse ~> po_eq_conv [THEN iffD1]

  box_less             ~> box_below

  rev_trans_less       ~> rev_below_trans

  not_less2not_eq      ~> not_below2not_eq

  less_UU_iff          ~> below_UU_iff

  flat_less_iff        ~> flat_below_iff

  adm_less             ~> adm_below

  adm_not_less         ~> adm_not_below

  adm_compact_not_less ~> adm_compact_not_below

  less_fun_def         ~> below_fun_def

  expand_fun_less      ~> fun_below_iff

  less_fun_ext         ~> fun_belowI

  less_discr_def       ~> below_discr_def

  discr_less_eq        ~> discr_below_eq

  less_unit_def        ~> below_unit_def

  less_cprod_def       ~> below_prod_def

  prod_lessI           ~> prod_belowI

  Pair_less_iff        ~> Pair_below_iff

  fst_less_iff         ~> fst_below_iff

  snd_less_iff         ~> snd_below_iff

  expand_cfun_less     ~> cfun_below_iff

  less_cfun_ext        ~> cfun_belowI

  injection_less       ~> injection_below

  less_up_def          ~> below_up_def

  not_Iup_less         ~> not_Iup_below

  Iup_less             ~> Iup_below

  up_less              ~> up_below

  Def_inject_less_eq   ~> Def_below_Def

  Def_less_is_eq       ~> Def_below_iff

  spair_less_iff       ~> spair_below_iff

  less_sprod           ~> below_sprod

  spair_less           ~> spair_below

  sfst_less_iff        ~> sfst_below_iff

  ssnd_less_iff        ~> ssnd_below_iff

  fix_least_less       ~> fix_least_below

  dist_less_one        ~> dist_below_one

  less_ONE             ~> below_ONE

  ONE_less_iff         ~> ONE_below_iff

  less_sinlD           ~> below_sinlD

  less_sinrD           ~> below_sinrD

*** FOL and ZF ***

* All constant names are now qualified internally and use proper

identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.

*** ML ***

* Antiquotation @{assert} inlines a function bool -> unit that raises

Fail if the argument is false.  Due to inlining the source position of

failed assertions is included in the error output.

* Discontinued antiquotation @{theory_ref}, which is obsolete since ML

text is in practice always evaluated with a stable theory checkpoint.

Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.

* Antiquotation @{theory A} refers to theory A from the ancestry of

the current context, not any accidental theory loader state as before.

Potential INCOMPATIBILITY, subtle change in semantics.

* Syntax.pretty_priority (default 0) configures the required priority

of pretty-printed output and thus affects insertion of parentheses.

* Syntax.default_root (default "any") configures the inner syntax

category (nonterminal symbol) for parsing of terms.

* Former exception Library.UnequalLengths now coincides with

ListPair.UnequalLengths.

* Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the

main functionality is provided by structure Simplifier.

* Renamed raw "explode" function to "raw_explode" to emphasize its

meaning.  Note that internally to Isabelle, Symbol.explode is used in

almost all situations.

* Discontinued obsolete function sys_error and exception SYS_ERROR.

See implementation manual for further details on exceptions in

Isabelle/ML.

* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its

meaning.

* Renamed structure PureThy to Pure_Thy and moved most of its

operations to structure Global_Theory, to emphasize that this is

rarely-used global-only stuff.

* Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln

instead (or tracing for high-volume output).

* Configuration option show_question_marks only affects regular pretty

printing of types and terms, not raw Term.string_of_vname.

* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare

INCOMPATIBILITY, superseded by static antiquotations @{thm} and

@{thms} for most purposes.

* ML structure Unsynchronized is never opened, not even in Isar

interaction mode as before.  Old Unsynchronized.set etc. have been

discontinued -- use plain := instead.  This should be *rare* anyway,

since modern tools always work via official context data, notably

configuration options.

* Parallel and asynchronous execution requires special care concerning

interrupts.  Structure Exn provides some convenience functions that

avoid working directly with raw Interrupt.  User code must not absorb

interrupts -- intermediate handling (for cleanup etc.) needs to be

followed by re-raising of the original exception.  Another common

source of mistakes are "handle _" patterns, which make the meaning of

the program subject to physical effects of the environment.

New in Isabelle2009-2 (June 2010)

---------------------------------

*** General ***

* Authentic syntax for *all* logical entities (type classes, type

constructors, term constants): provides simple and robust

correspondence between formal entities and concrete syntax.  Within

the parse tree / AST representations, "constants" are decorated by

their category (class, type, const) and spelled out explicitly with

their full internal name.

Substantial INCOMPATIBILITY concerning low-level syntax declarations

and translations (translation rules and translation functions in ML).

Some hints on upgrading:

  - Many existing uses of 'syntax' and 'translations' can be replaced

    by more modern 'type_notation', 'notation' and 'abbreviation',

    which are independent of this issue.

  - 'translations' require markup within the AST; the term syntax

    provides the following special forms:

      CONST c   -- produces syntax version of constant c from context

      XCONST c  -- literally c, checked as constant from context

      c         -- literally c, if declared by 'syntax'

    Plain identifiers are treated as AST variables -- occasionally the

    system indicates accidental variables via the error "rhs contains

    extra variables".

    Type classes and type constructors are marked according to their

    concrete syntax.  Some old translations rules need to be written

    for the "type" category, using type constructor application

    instead of pseudo-term application of the default category

    "logic".

  - 'parse_translation' etc. in ML may use the following

    antiquotations:

      @{class_syntax c}   -- type class c within parse tree / AST

      @{term_syntax c}    -- type constructor c within parse tree / AST

      @{const_syntax c}   -- ML version of "CONST c" above

      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)

  - Literal types within 'typed_print_translations', i.e. those *not*

    represented as pseudo-terms are represented verbatim.  Use @{class

    c} or @{type_name c} here instead of the above syntax

    antiquotations.

Note that old non-authentic syntax was based on unqualified base

names, so all of the above "constant" names would coincide.  Recall

that 'print_syntax' and ML_command "set Syntax.trace_ast" help to

diagnose syntax problems.

* Type constructors admit general mixfix syntax, not just infix.

* Concrete syntax may be attached to local entities without a proof

body, too.  This works via regular mixfix annotations for 'fix',

'def', 'obtain' etc. or via the explicit 'write' command, which is

similar to the 'notation' command in theory specifications.

* Discontinued unnamed infix syntax (legacy feature for many years) --

need to specify constant name and syntax separately.  Internal ML

datatype constructors have been renamed from InfixName to Infix etc.

Minor INCOMPATIBILITY.

* Schematic theorem statements need to be explicitly markup as such,

via commands 'schematic_lemma', 'schematic_theorem',

'schematic_corollary'.  Thus the relevance of the proof is made

syntactically clear, which impacts performance in a parallel or

asynchronous interactive environment.  Minor INCOMPATIBILITY.

* Use of cumulative prems via "!" in some proof methods has been

discontinued (old legacy feature).

* References 'trace_simp' and 'debug_simp' have been replaced by

configuration options stored in the context. Enabling tracing (the

case of debugging is similar) in proofs works via

  using [[trace_simp = true]]

Tracing is then active for all invocations of the simplifier in

subsequent goal refinement steps. Tracing may also still be enabled or

disabled via the ProofGeneral settings menu.

* Separate commands 'hide_class', 'hide_type', 'hide_const',

'hide_fact' replace the former 'hide' KIND command.  Minor

INCOMPATIBILITY.

* Improved parallelism of proof term normalization: usedir -p2 -q0 is

more efficient than combinations with -q1 or -q2.

*** Pure ***

* Proofterms record type-class reasoning explicitly, using the

"unconstrain" operation internally.  This eliminates all sort

constraints from a theorem and proof, introducing explicit

OFCLASS-premises.  On the proof term level, this operation is

automatically applied at theorem boundaries, such that closed proofs

are always free of sort constraints.  INCOMPATIBILITY for tools that

inspect proof terms.

* Local theory specifications may depend on extra type variables that

are not present in the result type -- arguments TYPE('a) :: 'a itself

are added internally.  For example:

  definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"

* Predicates of locales introduced by classes carry a mandatory

"class" prefix.  INCOMPATIBILITY.

* Vacuous class specifications observe default sort.  INCOMPATIBILITY.

* Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use

'class' instead.

* Command 'code_reflect' allows to incorporate generated ML code into

runtime environment; replaces immature code_datatype antiquotation.

INCOMPATIBILITY.

* Code generator: simple concept for abstract datatypes obeying

invariants.

* Code generator: details of internal data cache have no impact on the

user space functionality any longer.

* Methods "unfold_locales" and "intro_locales" ignore non-locale

subgoals.  This is more appropriate for interpretations with 'where'.

INCOMPATIBILITY.

* Command 'example_proof' opens an empty proof body.  This allows to

experiment with Isar, without producing any persistent result.

* Commands 'type_notation' and 'no_type_notation' declare type syntax

within a local theory context, with explicit checking of the

constructors involved (in contrast to the raw 'syntax' versions).

* Commands 'types' and 'typedecl' now work within a local theory

context -- without introducing dependencies on parameters or

assumptions, which is not possible in Isabelle/Pure.

* Command 'defaultsort' has been renamed to 'default_sort', it works

within a local theory context.  Minor INCOMPATIBILITY.

*** HOL ***

* Command 'typedef' now works within a local theory context -- without

introducing dependencies on parameters or assumptions, which is not

possible in Isabelle/Pure/HOL.  Note that the logical environment may

contain multiple interpretations of local typedefs (with different

non-emptiness proofs), even in a global theory context.

* New package for quotient types.  Commands 'quotient_type' and

'quotient_definition' may be used for defining types and constants by

quotient constructions.  An example is the type of integers created by

quotienting pairs of natural numbers:

  fun

    intrel :: "(nat * nat) => (nat * nat) => bool"

  where

    "intrel (x, y) (u, v) = (x + v = u + y)"

  quotient_type int = "nat * nat" / intrel

    by (auto simp add: equivp_def expand_fun_eq)

  quotient_definition

    "0::int" is "(0::nat, 0::nat)"

The method "lifting" can be used to lift of theorems from the

underlying "raw" type to the quotient type.  The example

src/HOL/Quotient_Examples/FSet.thy includes such a quotient

construction and provides a reasoning infrastructure for finite sets.

* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid

clash with new theory Quotient in Main HOL.

* Moved the SMT binding into the main HOL session, eliminating

separate HOL-SMT session.

* List membership infix mem operation is only an input abbreviation.

INCOMPATIBILITY.

* Theory Library/Word.thy has been removed.  Use library Word/Word.thy

for future developements; former Library/Word.thy is still present in

the AFP entry RSAPPS.

* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no

longer shadowed.  INCOMPATIBILITY.

* Dropped theorem duplicate comp_arith; use semiring_norm instead.

INCOMPATIBILITY.