Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

*** General ***

* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

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

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.

* Significantly improved Isabelle/Isar implementation manual.

* Explicit treatment of UTF8 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 loading: only the master source file is looked-up in the

implicit load path, all other files are addressed relatively to its

directory.  Minor INCOMPATIBILITY, subtle change in semantics.

* 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.  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

  Syntax.ambiguity_level        syntax_ambiguity_level

  Goal_Display.goals_limit      goals_limit

  Goal_Display.show_main_goal   show_main_goal

  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 be only

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

*** Pure ***

* 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).

* Interpretation command 'interpret' accepts a list of equations like

'interpretation' does.

* 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 ancient 'constdefs' command.  INCOMPATIBILITY, use

'definition' instead.

* Document antiquotations @{class} and @{type} for printing classes

and type constructors.

*** HOL ***

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

replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.

* Theory Enum (for explicit enumerations of finite types) 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.

  constants

    enum -> Enum.enum

    nlists -> Enum.nlists

    product -> Enum.product

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

avoid confusion with finite sets.  INCOMPATIBILITY.

* Quickcheck's generator for random generation is renamed from "code" to

"random".  INCOMPATIBILITY.

* Theory Multiset provides stable quicksort implementation of sort_key.

* 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.

* New 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

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

examples.

* Predicates `distinct` and `sorted` now defined inductively, with nice

induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps

now named distinct_simps and sorted_simps.

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

contents for other uses.  INCOMPATIBILITY.

* Dropped syntax for old primrec package.  INCOMPATIBILITY.

* Improved infrastructure for term evaluation using code generator

techniques, in particular static evaluation conversions.

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

* Renamed lemmas:

  expand_fun_eq -> fun_eq_iff

  expand_set_eq -> set_eq_iff

  set_ext -> set_eqI

 INCOMPATIBILITY.

* Renamed lemma list: nat_number -> eval_nat_numeral

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

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

INCOMPATIBILITY.

* Scala (2.8 or higher) has been added to the target languages of

the code generator.

* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

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

* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;

canonical names for instance definitions for functions; various improvements.

INCOMPATIBILITY.

* Records: logical foundation type for records do not carry a '_type' suffix

any longer.  INCOMPATIBILITY.

* Code generation 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 ...

* Session Imperative_HOL: revamped, corrected dozens of inadequacies.

INCOMPATIBILITY.

* Quickcheck in locales considers interpretations of that locale for

counter example search.

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

in Library/State_Monad has been changed to avoid ambiguities.

INCOMPATIBILITY.

* Code generator: export_code without explicit file declaration prints

to standard output.  INCOMPATIBILITY.

* Abolished symbol type names:  "prod" and "sum" replace "*" and "+"

respectively.  INCOMPATIBILITY.

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

  Write Sum_Type.Plus.

* 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 "in set"

instead.  INCOMPATIBILITY.

* Refactoring of code-generation specific operations in List.thy

  constants

    null ~> List.null

  facts

    mem_iff ~> member_def

    null_empty ~> null_def

INCOMPATIBILITY.  Note that these were not suppossed to be used

regularly unless for striking reasons;  their main purpose was code

generation.

* 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.

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

been the case with "split".  INCOMPATIBILITY.

* Datatype package: theorems generated for executable equality

(class eq) carry proper names and are treated as default code

equations.

* Removed lemma Option.is_none_none (Duplicate of is_none_def).

INCOMPATIBILITY.

* List.thy: use various operations from the Haskell prelude when

generating Haskell code.

* Multiset.thy: renamed empty_idemp -> empty_neutral

* code_simp.ML and method code_simp: simplification with rules determined

by code generator.

* code generator: do not print function definitions for case

combinators any longer.

* 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.

* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal

as value for measures. Introduces Lebesgue Measure based on the integral in

Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure

spaces.

 INCOMPATIBILITY.

* Inductive package: offers new command "inductive_simps" to automatically

derive instantiated and simplified equations for inductive predicates,

similar to inductive_cases.

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

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

surj_def are unchanged.  INCOMPATIBILITY.

* Function package: .psimps rules are no longer implicitly declared [simp].

INCOMPATIBILITY.

* Weaker versions of the "meson" and "metis" proof methods are now available in

  "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become

  more powerful after "Hilbert_Choice" is loaded in "HOL-Main".

* MESON: Renamed lemmas:

  meson_not_conjD ~> Meson.not_conjD

  meson_not_disjD ~> Meson.not_disjD

  meson_not_notD ~> Meson.not_notD

  meson_not_allD ~> Meson.not_allD

  meson_not_exD ~> Meson.not_exD

  meson_imp_to_disjD ~> Meson.imp_to_disjD

  meson_not_impD ~> Meson.not_impD

  meson_iff_to_disjD ~> Meson.iff_to_disjD

  meson_not_iffD ~> Meson.not_iffD

  meson_not_refl_disj_D ~> Meson.not_refl_disj_D

  meson_conj_exD1 ~> Meson.conj_exD1

  meson_conj_exD2 ~> Meson.conj_exD2

  meson_disj_exD ~> Meson.disj_exD

  meson_disj_exD1 ~> Meson.disj_exD1

  meson_disj_exD2 ~> Meson.disj_exD2

  meson_disj_assoc ~> Meson.disj_assoc

  meson_disj_comm ~> Meson.disj_comm

  meson_disj_FalseD1 ~> Meson.disj_FalseD1

  meson_disj_FalseD2 ~> Meson.disj_FalseD2

INCOMPATIBILITY.

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

  "solve_direct".

* Sledgehammer:

  - Added "smt" and "remote_smt" provers based on the "smt" proof method. See

    the Sledgehammer manual for details ("isabelle doc sledgehammer").

  - Renamed lemmas:

    COMBI_def ~> Meson.COMBI_def

    COMBK_def ~> Meson.COMBK_def

    COMBB_def ~> Meson.COMBB_def

    COMBC_def ~> Meson.COMBC_def

    COMBS_def ~> Meson.COMBS_def

    abs_I ~> Meson.abs_I

    abs_K ~> Meson.abs_K

    abs_B ~> Meson.abs_B

    abs_C ~> Meson.abs_C

    abs_S ~> Meson.abs_S

    INCOMPATIBILITY.

  - 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.

* 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]]

* Nitpick:

  - Renamed options:

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

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

    INCOMPATIBILITY.

  - Now requires Kodkodi 1.2.9. 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.

* Changed SMT configuration options:

  - Renamed:

    z3_proofs ~> smt_oracle (with swapped semantics)

    z3_trace_assms ~> smt_trace_used_facts

    INCOMPATIBILITY.

  - Added:

    smt_verbose

    smt_datatypes

    cvc3_options

    yices_options

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

theory header.

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

[split_format].  Potential INCOMPATIBILITY.

*** 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; the definitional

domain package and the powerdomain theories both require this class.

The new 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 old type classes 'profinite' and 'bifinite', along with the

overloaded constant 'approx' have been removed. INCOMPATIBILITY.

* The type 'udom alg_defl' has been replaced by the non-parameterized

type 'defl'. HOLCF no longer defines an embedding of type defl into

udom by default; the instance proof defl :: domain is now available in

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.

* 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.

* 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 ***

* All constant names are now qualified.  INCOMPATIBILITY.

*** ZF ***

* All constant names are now qualified.  INCOMPATIBILITY.

*** ML ***

* Former exception Library.UnequalLengths now coincides with

ListPair.UnequalLengths.

* 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.

* 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.

* 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 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.

* ML antiquotations @{theory} and @{theory_ref} refer to named

theories from the ancestry of the current context, not any accidental

theory loader state as before.  Potential INCOMPATIBILITY, subtle

change in semantics.

* 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.

*** System ***

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

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 Proof General 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.

* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.

INCOMPATIBILITY.

* Dropped normalizing_semiring etc; use the facts in semiring classes

instead.  INCOMPATIBILITY.

* Dropped several real-specific versions of lemmas about floor and

ceiling; use the generic lemmas from theory "Archimedean_Field"

instead.  INCOMPATIBILITY.

  floor_number_of_eq         ~> floor_number_of

  le_floor_eq_number_of      ~> number_of_le_floor

  le_floor_eq_zero           ~> zero_le_floor

  le_floor_eq_one            ~> one_le_floor

  floor_less_eq_number_of    ~> floor_less_number_of

  floor_less_eq_zero         ~> floor_less_zero

  floor_less_eq_one          ~> floor_less_one

  less_floor_eq_number_of    ~> number_of_less_floor

  less_floor_eq_zero         ~> zero_less_floor

  less_floor_eq_one          ~> one_less_floor

  floor_le_eq_number_of      ~> floor_le_number_of

  floor_le_eq_zero           ~> floor_le_zero

  floor_le_eq_one            ~> floor_le_one

  floor_subtract_number_of   ~> floor_diff_number_of

  floor_subtract_one         ~> floor_diff_one

  ceiling_number_of_eq       ~> ceiling_number_of

  ceiling_le_eq_number_of    ~> ceiling_le_number_of

  ceiling_le_zero_eq         ~> ceiling_le_zero

  ceiling_le_eq_one          ~> ceiling_le_one

  less_ceiling_eq_number_of  ~> number_of_less_ceiling

  less_ceiling_eq_zero       ~> zero_less_ceiling

  less_ceiling_eq_one        ~> one_less_ceiling

  ceiling_less_eq_number_of  ~> ceiling_less_number_of

  ceiling_less_eq_zero       ~> ceiling_less_zero

  ceiling_less_eq_one        ~> ceiling_less_one

  le_ceiling_eq_number_of    ~> number_of_le_ceiling

  le_ceiling_eq_zero         ~> zero_le_ceiling

  le_ceiling_eq_one          ~> one_le_ceiling

  ceiling_subtract_number_of ~> ceiling_diff_number_of

  ceiling_subtract_one       ~> ceiling_diff_one

* Theory "Finite_Set": various folding_XXX locales facilitate the

application of the various fold combinators on finite sets.

* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"

provides abstract red-black tree type which is backed by "RBT_Impl" as

implementation.  INCOMPATIBILTY.

* Theory Library/Coinductive_List has been removed -- superseded by

AFP/thys/Coinductive.

* Theory PReal, including the type "preal" and related operations, has

been removed.  INCOMPATIBILITY.

* Real: new development using Cauchy Sequences.

* Split off theory "Big_Operators" containing setsum, setprod,

Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

* Theory "Rational" renamed to "Rat", for consistency with "Nat",

"Int" etc.  INCOMPATIBILITY.

* Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.

* New set of rules "ac_simps" provides combined assoc / commute

rewrites for all interpretations of the appropriate generic locales.

* Renamed theory "OrderedGroup" to "Groups" and split theory

"Ring_and_Field" into theories "Rings" and "Fields"; for more

appropriate and more consistent names suitable for name prefixes

within the HOL theories.  INCOMPATIBILITY.

* Some generic constants have been put to appropriate theories:

  - less_eq, less: Orderings

  - zero, one, plus, minus, uminus, times, abs, sgn: Groups

  - inverse, divide: Rings

INCOMPATIBILITY.

* More consistent naming of type classes involving orderings (and

lattices):

    lower_semilattice                   ~> semilattice_inf

    upper_semilattice                   ~> semilattice_sup

    dense_linear_order                  ~> dense_linorder

    pordered_ab_group_add               ~> ordered_ab_group_add

    pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs

    pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add

    pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le

    pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add

    pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring

    pordered_cancel_semiring            ~> ordered_cancel_semiring

    pordered_comm_monoid_add            ~> ordered_comm_monoid_add

    pordered_comm_ring                  ~> ordered_comm_ring

    pordered_comm_semiring              ~> ordered_comm_semiring

    pordered_ring                       ~> ordered_ring

    pordered_ring_abs                   ~> ordered_ring_abs

    pordered_semiring                   ~> ordered_semiring

    ordered_ab_group_add                ~> linordered_ab_group_add

    ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add

    ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add

    ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict

    ordered_field                       ~> linordered_field

    ordered_field_no_lb                 ~> linordered_field_no_lb

    ordered_field_no_ub                 ~> linordered_field_no_ub

    ordered_field_dense_linear_order    ~> dense_linordered_field

    ordered_idom                        ~> linordered_idom

    ordered_ring                        ~> linordered_ring

    ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor

    ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor

    ordered_ring_strict                 ~> linordered_ring_strict

    ordered_semidom                     ~> linordered_semidom

    ordered_semiring                    ~> linordered_semiring

    ordered_semiring_1                  ~> linordered_semiring_1

    ordered_semiring_1_strict           ~> linordered_semiring_1_strict

    ordered_semiring_strict             ~> linordered_semiring_strict

  The following slightly odd type classes have been moved to a

  separate theory Library/Lattice_Algebras:

    lordered_ab_group_add               ~> lattice_ab_group_add

    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs

    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add

    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add

    lordered_ring                       ~> lattice_ring

INCOMPATIBILITY.

* Refined field classes:

  - classes division_ring_inverse_zero, field_inverse_zero,

    linordered_field_inverse_zero include rule inverse 0 = 0 --

    subsumes former division_by_zero class;

  - numerous lemmas have been ported from field to division_ring.

INCOMPATIBILITY.

* Refined algebra theorem collections:

  - dropped theorem group group_simps, use algebra_simps instead;

  - dropped theorem group ring_simps, use field_simps instead;

  - proper theorem collection field_simps subsumes former theorem

    groups field_eq_simps and field_simps;

  - dropped lemma eq_minus_self_iff which is a duplicate for

    equal_neg_zero.

INCOMPATIBILITY.

* Theory Finite_Set and List: some lemmas have been generalized from

sets to lattices:

  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf

  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup

  inter_Inter_fold_inter        ~> inf_Inf_fold_inf

  union_Union_fold_union        ~> sup_Sup_fold_sup

  Inter_fold_inter              ~> Inf_fold_inf

  Union_fold_union              ~> Sup_fold_sup

  inter_INTER_fold_inter        ~> inf_INFI_fold_inf

  union_UNION_fold_union        ~> sup_SUPR_fold_sup

  INTER_fold_inter              ~> INFI_fold_inf

  UNION_fold_union              ~> SUPR_fold_sup

* Theory "Complete_Lattice": lemmas top_def and bot_def have been

replaced by the more convenient lemmas Inf_empty and Sup_empty.

Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed

by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace

former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right

subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.

* Reorganized theory Multiset: swapped notation of pointwise and

multiset order:

  - pointwise ordering is instance of class order with standard syntax

    <= and <;

  - multiset ordering has syntax <=# and <#; partial order properties

    are provided by means of interpretation with prefix

    multiset_order;

  - less duplication, less historical organization of sections,

    conversion from associations lists to multisets, rudimentary code

    generation;

  - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,

    if needed.

Renamed:

  multiset_eq_conv_count_eq  ~>  multiset_ext_iff

  multi_count_ext  ~>  multiset_ext

  diff_union_inverse2  ~>  diff_union_cancelR

INCOMPATIBILITY.

* Theory Permutation: replaced local "remove" by List.remove1.

* Code generation: ML and OCaml code is decorated with signatures.

* Theory List: added transpose.

* Library/Nat_Bijection.thy is a collection of bijective functions

between nat and other types, which supersedes the older libraries

Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.

  Constants:

  Nat_Int_Bij.nat2_to_nat         ~> prod_encode

  Nat_Int_Bij.nat_to_nat2         ~> prod_decode

  Nat_Int_Bij.int_to_nat_bij      ~> int_encode

  Nat_Int_Bij.nat_to_int_bij      ~> int_decode

  Countable.pair_encode           ~> prod_encode

  NatIso.prod2nat                 ~> prod_encode

  NatIso.nat2prod                 ~> prod_decode

  NatIso.sum2nat                  ~> sum_encode

  NatIso.nat2sum                  ~> sum_decode

  NatIso.list2nat                 ~> list_encode

  NatIso.nat2list                 ~> list_decode

  NatIso.set2nat                  ~> set_encode

  NatIso.nat2set                  ~> set_decode