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.

*** 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 orderes.  Lemmas Inf_less_iff,

less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.

More consistent and less misunderstandable names:

  INFI_def ~> INF_def

  SUPR_def ~> SUP_def

  le_SUPI ~> le_SUP_I

  le_SUPI2 ~> le_SUP_I2

  le_INFI ~> le_INF_I

  INFI_bool_eq ~> INF_bool_eq

  SUPR_bool_eq ~> SUP_bool_eq

  INFI_apply ~> INF_apply

  SUPR_apply ~> SUP_apply

INCOMPATIBILITY.

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

  - evaluator "SML" and method evaluation are legacy, use evaluator "code"

    and method eval instead.

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

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

* 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