Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

*** General ***

* Theory loader: source files are identified by content via SHA1

digests.  Discontinued former path/modtime identification and optional

ISABELLE_FILE_IDENT plugin scripts.

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

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

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

The global load path (such as src/HOL/Library) has been discontinued.

Note that the path element ~~ may be used to reference theories in the

Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".

INCOMPATIBILITY.

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

  long_names   ~> names_long

  short_names  ~> names_short

  unique_names ~> names_unique

Minor INCOMPATIBILITY, need to declare options in context like this:

  declare [[names_unique = false]]

* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note

that the result needs to be unique, which means fact specifications

may have to be refined after enriching a proof context.

* Isabelle/Isar reference manual provides more formal references in

syntax diagrams.

* Attribute case_names has been refined: the assumptions in each case can

be named now by following the case name with [name1 name2 ...].

*** HOL ***

* Classes bot and top require underlying partial order rather than preorder:

uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.

* Class complete_lattice: generalized a couple of lemmas from sets;

generalized theorems INF_cong and SUP_cong.  New type classes for complete

boolean algebras and complete linear orders.  Lemmas Inf_less_iff,

less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.

Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def,

Inf_apply, Sup_apply.

Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,

INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,

INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,

Union_def, UN_singleton, UN_eq have been discarded.

More consistent and less misunderstandable names:

  INFI_def ~> INF_def

  SUPR_def ~> SUP_def

  INF_leI ~> INF_lower

  INF_leI2 ~> INF_lower2

  le_INFI ~> INF_greatest

  le_SUPI ~> SUP_upper

  le_SUPI2 ~> SUP_upper2

  SUP_leI ~> SUP_least

  INFI_bool_eq ~> INF_bool_eq

  SUPR_bool_eq ~> SUP_bool_eq

  INFI_apply ~> INF_apply

  SUPR_apply ~> SUP_apply

  INTER_def ~> INTER_eq

  UNION_def ~> UNION_eq

INCOMPATIBILITY.

* Theorem collections ball_simps and bex_simps do not contain theorems referring

to UNION any longer;  these have been moved to collection UN_ball_bex_simps.

INCOMPATIBILITY.

* Archimedean_Field.thy:

    floor now is defined as parameter of a separate type class floor_ceiling.

* Finite_Set.thy: more coherent development of fold_set locales:

    locale fun_left_comm ~> locale comp_fun_commute

    locale fun_left_comm_idem ~> locale comp_fun_idem

Both use point-free characterisation; interpretation proofs may need adjustment.

INCOMPATIBILITY.

* Code generation:

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

  - method evaluation is legacy, use method eval instead.

  - legacy evaluator "SML" is deactivated by default. To activate it, add the following

    line in your theory:

      setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}

* Declare ext [intro] by default.  Rare INCOMPATIBILITY.

* Nitpick:

  - Added "need" and "total_consts" options.

  - Reintroduced "show_skolems" option by popular demand.

  - Renamed attribute: nitpick_def ~> nitpick_unfold.

    INCOMPATIBILITY.

* Sledgehammer:

  - sledgehammer available_provers ~> sledgehammer supported_provers.

    INCOMPATIBILITY.

  - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed

    TPTP problems (TFF).

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

* "try":

  - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"

    options. INCOMPATIBILITY.

  - Introduced "try" that not only runs "try_methods" but also "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.

    It requires that the Glasgow Haskell compiler is installed and

    its location is known to Isabelle with the environment variable

    ISABELLE_GHC.

  - Removed quickcheck tester "SML" based on the SML code generator

    from HOL-Library

* Function package: discontinued option "tailrec".

INCOMPATIBILITY. Use partial_function instead.

* HOL-Probability:

  - Caratheodory's extension lemma is now proved for ring_of_sets.

  - Infinite products of probability measures are now available.

  - Use extended reals instead of positive extended reals.

    INCOMPATIBILITY.

* Old recdef package has been moved to Library/Old_Recdef.thy, where it

must be loaded explicitly.  INCOMPATIBILITY.

* Well-founded recursion combinator "wfrec" has been moved to

Library/Wfrec.thy. INCOMPATIBILITY.

* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat.

The names of the following types and constants have changed:

  inat (type) ~> enat

  Fin         ~> enat

  Infty       ~> infinity (overloaded)

  iSuc        ~> eSuc

  the_Fin     ~> the_enat

Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has

been renamed accordingly.

* Limits.thy: Type "'a net" has been renamed to "'a filter", in

accordance with standard mathematical terminology. INCOMPATIBILITY.

* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed

to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants

"Cart_nth" and "Cart_lambda" have been respectively renamed to

"vec_nth" and "vec_lambda"; theorems mentioning those names have

changed to match. Definition theorems for overloaded constants now use

the standard "foo_vec_def" naming scheme. A few other theorems have

been renamed as follows (INCOMPATIBILITY):

  Cart_eq          ~> vec_eq_iff

  dist_nth_le_cart ~> dist_vec_nth_le

  tendsto_vector   ~> vec_tendstoI

  Cauchy_vector    ~> vec_CauchyI

* Session Multivariate_Analysis: Several duplicate theorems have been

removed, and other theorems have been renamed or replaced with more

general versions. INCOMPATIBILITY.

  finite_choice ~> finite_set_choice

  eventually_conjI ~> eventually_conj

  eventually_and ~> eventually_conj_iff

  eventually_false ~> eventually_False

  setsum_norm ~> norm_setsum

  Lim_ident_at ~> LIM_ident

  Lim_const ~> tendsto_const

  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

  Lim_neg ~> tendsto_minus

  Lim_add ~> tendsto_add

  Lim_sub ~> tendsto_diff

  Lim_mul ~> tendsto_scaleR

  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

  Lim_linear ~> bounded_linear.tendsto

  Lim_component ~> tendsto_euclidean_component

  Lim_component_cart ~> tendsto_vec_nth

  Lim_inner ~> tendsto_inner [OF tendsto_const]

  dot_lsum ~> inner_setsum_left

  dot_rsum ~> inner_setsum_right

  continuous_cmul ~> continuous_scaleR [OF continuous_const]

  continuous_neg ~> continuous_minus

  continuous_sub ~> continuous_diff

  continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

  continuous_mul ~> continuous_scaleR

  continuous_inv ~> continuous_inverse

  continuous_at_within_inv ~> continuous_at_within_inverse

  continuous_at_inv ~> continuous_at_inverse

  continuous_at_norm ~> continuous_norm [OF continuous_at_id]

  continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

  continuous_at_component ~> continuous_component [OF continuous_at_id]

  continuous_on_neg ~> continuous_on_minus

  continuous_on_sub ~> continuous_on_diff

  continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

  continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

  continuous_on_mul ~> continuous_on_scaleR

  continuous_on_mul_real ~> continuous_on_mult

  continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

  continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

  continuous_on_inverse ~> continuous_on_inv

  uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

  uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

  subset_interior ~> interior_mono

  subset_closure ~> closure_mono

  closure_univ ~> closure_UNIV

  real_arch_lt ~> reals_Archimedean2

  real_arch ~> reals_Archimedean3

  real_abs_norm ~> abs_norm_cancel

  real_abs_sub_norm ~> norm_triangle_ineq3

  norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

* Complex_Main: The locale interpretations for the bounded_linear and

bounded_bilinear locales have been removed, in order to reduce the

number of duplicate lemmas. Users must use the original names for

distributivity theorems, potential INCOMPATIBILITY.

  divide.add ~> add_divide_distrib

  divide.diff ~> diff_divide_distrib

  divide.setsum ~> setsum_divide_distrib

  mult.add_right ~> right_distrib

  mult.diff_right ~> right_diff_distrib

  mult_right.setsum ~> setsum_right_distrib

  mult_left.diff ~> left_diff_distrib

* Complex_Main: Several redundant theorems have been removed or

replaced by more general versions. INCOMPATIBILITY.

  real_0_le_divide_iff ~> zero_le_divide_iff

  realpow_two_disj ~> power2_eq_iff

  real_squared_diff_one_factored ~> square_diff_one_factored

  realpow_two_diff ~> square_diff_square_factored

  reals_complete2 ~> complete_real

  exp_ln_eq ~> ln_unique

  lemma_DERIV_subst ~> DERIV_cong

  LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

  LIMSEQ_const ~> tendsto_const

  LIMSEQ_norm ~> tendsto_norm

  LIMSEQ_add ~> tendsto_add

  LIMSEQ_minus ~> tendsto_minus

  LIMSEQ_minus_cancel ~> tendsto_minus_cancel

  LIMSEQ_diff ~> tendsto_diff

  bounded_linear.LIMSEQ ~> bounded_linear.tendsto

  bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

  LIMSEQ_mult ~> tendsto_mult

  LIMSEQ_inverse ~> tendsto_inverse

  LIMSEQ_divide ~> tendsto_divide

  LIMSEQ_pow ~> tendsto_power

  LIMSEQ_setsum ~> tendsto_setsum

  LIMSEQ_setprod ~> tendsto_setprod

  LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

  LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

  LIMSEQ_imp_rabs ~> tendsto_rabs

  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

  LIM_ident ~> tendsto_ident_at

  LIM_const ~> tendsto_const

  LIM_add ~> tendsto_add

  LIM_add_zero ~> tendsto_add_zero

  LIM_minus ~> tendsto_minus

  LIM_diff ~> tendsto_diff

  LIM_norm ~> tendsto_norm

  LIM_norm_zero ~> tendsto_norm_zero

  LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

  LIM_norm_zero_iff ~> tendsto_norm_zero_iff

  LIM_rabs ~> tendsto_rabs

  LIM_rabs_zero ~> tendsto_rabs_zero

  LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

  LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

  LIM_compose ~> tendsto_compose

  LIM_mult ~> tendsto_mult

  LIM_scaleR ~> tendsto_scaleR

  LIM_of_real ~> tendsto_of_real

  LIM_power ~> tendsto_power

  LIM_inverse ~> tendsto_inverse

  LIM_sgn ~> tendsto_sgn

  isCont_LIM_compose ~> isCont_tendsto_compose

  bounded_linear.LIM ~> bounded_linear.tendsto

  bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

  bounded_bilinear.LIM ~> bounded_bilinear.tendsto

  bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

  bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

  bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

  LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

*** Document preparation ***

* Discontinued special treatment of hard tabulators, which are better

avoided in the first place.  Implicit tab-width is 1.

* Antiquotation @{rail} layouts railroad syntax diagrams, see also

isar-ref manual.

* Antiquotation @{value} evaluates the given term and presents its result.

* Localized \isabellestyle switch can be used within blocks or groups

like this:

  \isabellestyle{it}  %preferred default

  {\isabellestylett @{text "typewriter stuff"}}

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

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

* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>

(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).

*** ML ***

* The inner syntax of sort/type/term/prop supports inlined YXML

representations within quoted string tokens.  By encoding logical

entities via Term_XML (in ML or Scala) concrete syntax can be

bypassed, which is particularly useful for producing bits of text

under external program control.

* Antiquotations for ML and document preparation are managed as theory

data, which requires explicit setup.

* Isabelle_Process.is_active allows tools to check if the official

process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop

(better known as Proof General).

* Structure Proof_Context follows standard naming scheme.  Old

ProofContext is still available for some time as legacy alias.

* Structure Timing provides various operations for timing; supersedes

former start_timing/end_timing etc.

* Path.print is the official way to show file-system paths to users

(including quotes etc.).

* Inner syntax: identifiers in parse trees of generic categories

"logic", "aprop", "idt" etc. carry position information (disguised as

type constraints).  Occasional INCOMPATIBILITY with non-compliant

translations that choke on unexpected type constraints.  Positions can

be stripped in ML translations via Syntax.strip_positions /

Syntax.strip_positions_ast, or via the syntax constant

"_strip_positions" within parse trees.  As last resort, positions can

be disabled via the configuration option Syntax.positions, which is

called "syntax_positions" in Isar attribute syntax.

* Discontinued special status of various ML structures that contribute

to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less

pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,

refer directly to Ast.Constant, Lexicon.is_identifier,

Syntax_Trans.mk_binder_tr etc.

* Typed print translation: discontinued show_sorts argument, which is

already available via context of "advanced" translation.

* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic

goal states; body tactic needs to address all subgoals uniformly.

* Slightly more special eq_list/eq_set, with shortcut involving

pointer equality (assumes that eq relation is reflexive).

* Classical tactics use proper Proof.context instead of historic types

claset/clasimpset.  Old-style declarations like addIs, addEs, addDs

operate directly on Proof.context.  Raw type claset retains its use as

snapshot of the classical context, which can be recovered via

(put_claset HOL_cs) etc.  Type clasimpset has been discontinued.

INCOMPATIBILITY, classical tactics and derived proof methods require

proper Proof.context.

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

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