Isabelle NEWS -- history user-relevant changes

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

New in this Isabelle version

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

*** General ***

* Uniform management of "quick_and_dirty" as system option (see also

"isabelle options"), configuration option within the context (see also

Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor

INCOMPATIBILITY, need to use more official Isabelle means to access

quick_and_dirty, instead of historical poking into mutable reference.

* Renamed command 'print_configs' to 'print_options'.  Minor

INCOMPATIBILITY.

* Sessions may be organized via 'chapter' specifications in the ROOT

file, which determines a two-level hierarchy of browser info.  The old

tree-like organization via implicit sub-session relation, with its

tendency towards erratic fluctuation of URLs, has been discontinued.

The default chapter is "Unsorted".  Potential INCOMPATIBILITY for HTML

presentation of theories.

* Discontinued obsolete 'uses' within theory header.  Note that

commands like 'ML_file' work without separate declaration of file

dependencies.  Minor INCOMPATIBILITY.

* Discontinued redundant 'use' command, which was superseded by

'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.

* Updated and extended "isar-ref" and "implementation" manual,

eliminated old "ref" manual.

* Proper diagnostic command 'print_state'.  Old 'pr' (with its

implicit change of some global references) is retained for now as

control command, e.g. for ProofGeneral 3.7.x.

* Discontinued 'print_drafts' command with its old-fashioned PS output

and Unix command-line print spooling.  Minor INCOMPATIBILITY: use

'display_drafts' instead and print via the regular document viewer.

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved "Theories" panel: Continuous checking of proof document

(visible and required parts) may be controlled explicitly, using check

box or shortcut "C+e ENTER".  Individual theory nodes may be marked

explicitly as required and checked in full, using check box or

shortcut "C+e SPACE".

* Strictly monotonic document update, without premature cancelation of

running transactions that are still needed: avoid reset/restart of

such command executions while editing.

* Support for asynchronous print functions, as overlay to existing

document content.

* Support for automatic tools in HOL, which try to prove or disprove

toplevel theorem statements.

* Dockable window "Documentation" provides access to Isabelle

documentation.

* Dockable window "Timing" provides an overview of relevant command

timing information.

* Option to skip over proofs, using implicit 'sorry' internally.

*** Pure ***

* Type theory is now immutable, without any special treatment of

drafts or linear updates (which could lead to "stale theory" errors in

the past).  Discontinued obsolete operations like Theory.copy,

Theory.checkpoint, and the auxiliary type theory_ref.  Minor

INCOMPATIBILITY.

* System option "proofs" has been discontinued.  Instead the global

state of Proofterm.proofs is persistently compiled into logic images

as required, notably HOL-Proofs.  Users no longer need to change

Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.

* Syntax translation functions (print_translation etc.) always depend

on Proof.context.  Discontinued former "(advanced)" option -- this is

now the default.  Minor INCOMPATIBILITY.

* Target-sensitive commands 'interpretation' and 'sublocale'.

Particulary, 'interpretation' now allows for non-persistent

interpretation within "context ... begin ... end" blocks.

See "isar-ref" manual for details.

* Improved locales diagnostic command 'print_dependencies'.

* Discontinued obsolete 'axioms' command, which has been marked as

legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'

instead, while observing its uniform scope for polymorphism.

* Discontinued empty name bindings in 'axiomatization'.

INCOMPATIBILITY.

* SELECT_GOAL now retains the syntactic context of the overall goal

state (schematic variables etc.).  Potential INCOMPATIBILITY in rare

situations.

*** HOL ***

* Improved support for adhoc overloading of constants (see also

isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.

Use explicit 'code equation' and 'code abstract' to distinguish both when desired.

* Code generator:

  * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.

  * 'code_identifier' declares name hints for arbitrary identifiers in generated code,

    subsuming 'code_modulename'.

  See the Isar reference manual for syntax diagrams, and the HOL theories for examples.

* Library/Polynomial.thy:

  * Use lifting for primitive definitions.

  * Explicit conversions from and to lists of coefficients, used for generated code.

  * Replaced recursion operator poly_rec by fold_coeffs.

  * Prefer pre-existing gcd operation for gcd.

  * Fact renames:

    poly_eq_iff ~> poly_eq_poly_eq_iff

    poly_ext ~> poly_eqI

    expand_poly_eq ~> poly_eq_iff

IMCOMPATIBILTIY.

* Reification and reflection:

  * Reification is now directly available in HOL-Main in structure "Reification".

  * Reflection now handles multiple lists with variables also.

  * The whole reflection stack has been decomposed into conversions.

INCOMPATIBILITY.

* Weaker precendence of syntax for big intersection and union on sets,

in accordance with corresponding lattice operations.  INCOMPATIBILITY.

* Nested case expressions are now translated in a separate check

  phase rather than during parsing. The data for case combinators

  is separated from the datatype package. The declaration attribute

  "case_translation" can be used to register new case combinators:

  declare [[case_translation case_combinator constructor1 ... constructorN]]

* Notation "{p:A. P}" now allows tuple patterns as well.

* Revised devices for recursive definitions over finite sets:

  - Only one fundamental fold combinator on finite set remains:

    Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b

    This is now identity on infinite sets.

  - Locales ("mini packages") for fundamental definitions with

    Finite_Set.fold: folding, folding_idem.

  - Locales comm_monoid_set, semilattice_order_set and

    semilattice_neutr_order_set for big operators on sets.

    See theory Big_Operators for canonical examples.

    Note that foundational constants comm_monoid_set.F and

    semilattice_set.F correspond to former combinators fold_image

    and fold1 respectively.  These are now gone.  You may use

    those foundational constants as substitutes, but it is

    preferable to interpret the above locales accordingly. 

  - Dropped class ab_semigroup_idem_mult (special case of lattice,

    no longer needed in connection with Finite_Set.fold etc.)

  - Fact renames:

      card.union_inter ~> card_Un_Int [symmetric]

      card.union_disjoint ~> card_Un_disjoint

INCOMPATIBILITY.

* Locale hierarchy for abstract orderings and (semi)lattices.

* Discontinued theory src/HOL/Library/Eval_Witness.

INCOMPATIBILITY.

* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since

Isabelle2013).  Use "isabelle build" to operate on Isabelle sessions.

* Numeric types mapped by default to target language numerals:

natural (replaces former code_numeral) and integer (replaces

former code_int).  Conversions are available as integer_of_natural /

natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and

Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML).

INCOMPATIBILITY.

* Discontinued theories Code_Integer and Efficient_Nat by a more

fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,

Code_Target_Nat and Code_Target_Numeral.  See the tutorial on

code generation for details.  INCOMPATIBILITY.

* Introduce type class "conditionally_complete_lattice": Like a complete

  lattice but does not assume the existence of the top and bottom elements.

  Allows to generalize some lemmas about reals and extended reals.

  Removed SupInf and replaced it by the instantiation of

  conditionally_complete_lattice for real. Renamed lemmas about

  conditionally-complete lattice from Sup_... to cSup_... and from Inf_...

  to cInf_... to avoid hidding of similar complete lattice lemmas.

  Introduce type class linear_continuum as combination of conditionally-complete

  lattices and inner dense linorders which have more than one element.

INCOMPATIBILITY.

* Introduce type classes "no_top" and "no_bot" for orderings without top

  and bottom elements.

* Split dense_linorder into inner_dense_order and no_top, no_bot.

* Complex_Main: Unify and move various concepts from

  HOL-Multivariate_Analysis to HOL-Complex_Main.

 - Introduce type class (lin)order_topology and linear_continuum_topology.

   Allows to generalize theorems about limits and order.

   Instances are reals and extended reals.

 - continuous and continuos_on from Multivariate_Analysis:

   "continuous" is the continuity of a function at a filter.

   "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f".

   Generalized continuity lemmas from isCont to continuous on an arbitrary

   filter.

 - compact from Multivariate_Analysis. Use Bolzano's lemma

   to prove compactness of closed intervals on reals. Continuous functions

   attain infimum and supremum on compact sets. The inverse of a continuous

   function is continuous, when the function is continuous on a compact set.

 - connected from Multivariate_Analysis. Use it to prove the

   intermediate value theorem. Show connectedness of intervals on

   linear_continuum_topology).

 - first_countable_topology from Multivariate_Analysis. Is used to

   show equivalence of properties on the neighbourhood filter of x and on

   all sequences converging to x.

 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems

   from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on

   FDERIV. Add variants of DERIV and FDERIV which are restricted to sets,

   i.e. to represent derivatives from left or right.

 - Removed the within-filter. It is replaced by the principal filter:

     F within X = inf F (principal X)

 - Introduce "at x within U" as a single constant, "at x" is now an

   abbreviation for "at x within UNIV"

 - Introduce named theorem collections tendsto_intros, continuous_intros,

   continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or

   FDERIV_intros) are also available as tendsto_eq_intros (or

   FDERIV_eq_intros) where the right-hand side is replaced by a congruence

   rule. This allows to apply them as intro rules and then proving

   equivalence by the simplifier.

 - Restructured theories in HOL-Complex_Main:

   + Moved RealDef and RComplete into Real

   + Introduced Topological_Spaces and moved theorems about

     topological spaces, filters, limits and continuity to it

   + Renamed RealVector to Real_Vector_Spaces

   + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and

     Limits

   + Moved Ln and Log to Transcendental

   + Moved theorems about continuity from Deriv to Topological_Spaces

 - Remove various auxiliary lemmas.

INCOMPATIBILITY.

* Consolidation of library theories on product orders:

    Product_Lattice ~> Product_Order -- pointwise order on products

    Product_ord ~> Product_Lexorder -- lexicographic order on products

INCOMPATIBILITY.

* Sledgehammer:

  - Renamed option:

      isar_shrink ~> isar_compress

* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.

  With HOL-Spec_Check, ML developers can check specifications with the

  ML function check_property. The specifications must be of the form

  "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in

  src/HOL/Spec_Check/Examples.thy.

*** HOL-Algebra ***

* Discontinued theories src/HOL/Algebra/abstract and .../poly.

Existing theories should be based on src/HOL/Library/Polynomial

instead.  The latter provides integration with HOL's type classes for

rings.  INCOMPATIBILITY.

*** ML ***

* More uniform naming of goal functions for skipped proofs:

    Skip_Proof.prove  ~>  Goal.prove_sorry

    Skip_Proof.prove_global  ~>  Goal.prove_sorry_global

* Antiquotation @{theory_context A} is similar to @{theory A}, but

presents the result as initial Proof.context.

* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)

operate on Proof.context instead of claset, for uniformity with addIs,

addEs, addDs etc. Note that claset_of and put_claset allow to manage

clasets separately from the context.

* Simplifier tactics and tools use proper Proof.context instead of

historic type simpset.  Old-style declarations like addsimps,

addsimprocs etc. operate directly on Proof.context.  Raw type simpset

retains its use as snapshot of the main Simplifier context, using

simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port

old tools by making them depend on (ctxt : Proof.context) instead of

(ss : simpset), then turn (simpset_of ctxt) into ctxt.

* Discontinued obsolete ML antiquotations @{claset} and @{simpset}.

INCOMPATIBILITY, use @{context} instead.

*** System ***

* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by

"isabelle build" in Isabelle2013.  INCOMPATIBILITY.

* Discontinued obsolete isabelle-process options -f and -u (former

administrative aliases of option -e).  Minor INCOMPATIBILITY.

* Discontinued obsolete isabelle print tool, and PRINT_COMMAND

settings variable.

* Discontinued ISABELLE_DOC_FORMAT settings variable and historic

document formats: dvi.gz, ps, ps.gz -- the default document format is

always pdf.

* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to

specify global resources of the JVM process run by isabelle build.

* Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows

to run Isabelle/Scala source files as standalone programs.

* Improved "isabelle keywords" tool (for old-style ProofGeneral

keyword tables): use Isabelle/Scala operations, which inspect outer

syntax without requiring to build sessions first.

New in Isabelle2013 (February 2013)

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

*** General ***

* Theorem status about oracles and unfinished/failed future proofs is

no longer printed by default, since it is incompatible with

incremental / parallel checking of the persistent document model.  ML

function Thm.peek_status may be used to inspect a snapshot of the

ongoing evaluation process.  Note that in batch mode --- notably

isabelle build --- the system ensures that future proofs of all

accessible theorems in the theory context are finished (as before).

* Configuration option show_markup controls direct inlining of markup

into the printed representation of formal entities --- notably type

and sort constraints.  This enables Prover IDE users to retrieve that

information via tooltips in the output window, for example.

* Command 'ML_file' evaluates ML text from a file directly within the

theory, without any predeclaration via 'uses' in the theory header.

* Old command 'use' command and corresponding keyword 'uses' in the

theory header are legacy features and will be discontinued soon.

Tools that load their additional source files may imitate the

'ML_file' implementation, such that the system can take care of

dependencies properly.

* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which

is called fastforce / fast_force_tac already since Isabelle2011-1.

* Updated and extended "isar-ref" and "implementation" manual, reduced

remaining material in old "ref" manual.

* Improved support for auxiliary contexts that indicate block structure

for specifications.  Nesting of "context fixes ... context assumes ..."

and "class ... context ...".

* Attribute "consumes" allows a negative value as well, which is

interpreted relatively to the total number of premises of the rule in

the target context.  This form of declaration is stable when exported

from a nested 'context' with additional assumptions.  It is the

preferred form for definitional packages, notably cases/rules produced

in HOL/inductive and HOL/function.

* More informative error messages for Isar proof commands involving

lazy enumerations (method applications etc.).

* Refined 'help' command to retrieve outer syntax commands according

to name patterns (with clickable results).

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Parallel terminal proofs ('by') are enabled by default, likewise

proofs that are built into packages like 'datatype', 'function'.  This

allows to "run ahead" checking the theory specifications on the

surface, while the prover is still crunching on internal

justifications.  Unfinished / cancelled proofs are restarted as

required to complete full proof checking eventually.

* Improved output panel with tooltips, hyperlinks etc. based on the

same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of

tooltips leads to some window that supports the same recursively,

which can lead to stacks of tooltips as the semantic document content

is explored.  ESCAPE closes the whole stack, individual windows may be

closed separately, or detached to become independent jEdit dockables.

* Improved support for commands that produce graph output: the text

message contains a clickable area to open a new instance of the graph

browser on demand.

* More robust incremental parsing of outer syntax (partial comments,

malformed symbols).  Changing the balance of open/close quotes and

comment delimiters works more conveniently with unfinished situations

that frequently occur in user interaction.

* More efficient painting and improved reactivity when editing large

files.  More scalable management of formal document content.

* Smarter handling of tracing messages: prover process pauses after

certain number of messages per command transaction, with some user

dialog to stop or continue.  This avoids swamping the front-end with

potentially infinite message streams.

* More plugin options and preferences, based on Isabelle/Scala.  The

jEdit plugin option panel provides access to some Isabelle/Scala

options, including tuning parameters for editor reactivity and color

schemes.

* Dockable window "Symbols" provides some editing support for Isabelle

symbols.

* Dockable window "Monitor" shows ML runtime statistics.  Note that

continuous display of the chart slows down the system.

* Improved editing support for control styles: subscript, superscript,

bold, reset of style -- operating on single symbols or text

selections.  Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.

* Actions isabelle.increase-font-size and isabelle.decrease-font-size

adjust the main text area font size, and its derivatives for output,

tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often

need to be adapted to local keyboard layouts.

* More reactive completion popup by default: use \t (TAB) instead of

\n (NEWLINE) to minimize intrusion into regular flow of editing.  See

also "Plugin Options / SideKick / General / Code Completion Options".

* Implicit check and build dialog of the specified logic session

image.  For example, HOL, HOLCF, HOL-Nominal can be produced on

demand, without bundling big platform-dependent heap images in the

Isabelle distribution.

* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates

from Oracle provide better multi-platform experience.  This version is

now bundled exclusively with Isabelle.

*** Pure ***

* Code generation for Haskell: restrict unqualified imports from

Haskell Prelude to a small set of fundamental operations.

* Command 'export_code': relative file names are interpreted

relatively to master directory of current theory rather than the

rather arbitrary current working directory.  INCOMPATIBILITY.

* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,

use regular rule composition via "OF" / "THEN", or explicit proof

structure instead.  Note that Isabelle/ML provides a variety of

operators like COMP, INCR_COMP, COMP_INCR, which need to be applied

with some care where this is really required.

* Command 'typ' supports an additional variant with explicit sort

constraint, to infer and check the most general type conforming to a

given sort.  Example (in HOL):

  typ "_ * _ * bool * unit" :: finite

* Command 'locale_deps' visualizes all locales and their relations as

a Hasse diagram.

*** HOL ***

* Sledgehammer:

  - Added MaSh relevance filter based on machine-learning; see the

    Sledgehammer manual for details.

  - Polished Isar proofs generated with "isar_proofs" option.

  - Rationalized type encodings ("type_enc" option).

  - Renamed "kill_provers" subcommand to "kill_all".

  - Renamed options:

      isar_proof ~> isar_proofs

      isar_shrink_factor ~> isar_shrink

      max_relevant ~> max_facts

      relevance_thresholds ~> fact_thresholds

* Quickcheck: added an optimisation for equality premises.  It is

switched on by default, and can be switched off by setting the

configuration quickcheck_optimise_equality to false.

* Quotient: only one quotient can be defined by quotient_type

INCOMPATIBILITY.

* Lifting:

  - generation of an abstraction function equation in lift_definition

  - quot_del attribute

  - renamed no_abs_code -> no_code (INCOMPATIBILITY.)

* Simproc "finite_Collect" rewrites set comprehensions into pointfree

expressions.

* Preprocessing of the code generator rewrites set comprehensions into

pointfree expressions.

* The SMT solver Z3 has now by default a restricted set of directly

supported features. For the full set of features (div/mod, nonlinear

arithmetic, datatypes/records) with potential proof reconstruction

failures, enable the configuration option "z3_with_extensions".  Minor

INCOMPATIBILITY.

* Simplified 'typedef' specifications: historical options for implicit

set definition and alternative name have been discontinued.  The

former behavior of "typedef (open) t = A" is now the default, but

written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories

accordingly.

* Removed constant "chars"; prefer "Enum.enum" on type "char"

directly.  INCOMPATIBILITY.

* Moved operation product, sublists and n_lists from theory Enum to

List.  INCOMPATIBILITY.

* Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.

* Class "comm_monoid_diff" formalises properties of bounded

subtraction, with natural numbers and multisets as typical instances.

* Added combinator "Option.these" with type "'a option set => 'a set".

* Theory "Transitive_Closure": renamed lemmas

  reflcl_tranclp -> reflclp_tranclp

  rtranclp_reflcl -> rtranclp_reflclp

INCOMPATIBILITY.

* Theory "Rings": renamed lemmas (in class semiring)

  left_distrib ~> distrib_right

  right_distrib ~> distrib_left

INCOMPATIBILITY.

* Generalized the definition of limits:

  - Introduced the predicate filterlim (LIM x F. f x :> G) which

    expresses that when the input values x converge to F then the

    output f x converges to G.

  - Added filters for convergence to positive (at_top) and negative

    infinity (at_bot).

  - Moved infinity in the norm (at_infinity) from

    Multivariate_Analysis to Complex_Main.

  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>

    at_top".

INCOMPATIBILITY.

* Theory "Library/Option_ord" provides instantiation of option type to

lattice type classes.

* Theory "Library/Multiset": renamed

    constant fold_mset ~> Multiset.fold

    fact fold_mset_commute ~> fold_mset_comm

INCOMPATIBILITY.

* Renamed theory Library/List_Prefix to Library/Sublist, with related

changes as follows.

  - Renamed constants (and related lemmas)

      prefix ~> prefixeq

      strict_prefix ~> prefix

  - Replaced constant "postfix" by "suffixeq" with swapped argument

    order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped

    old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.

    Renamed lemmas accordingly.

  - Added constant "list_hembeq" for homeomorphic embedding on

    lists. Added abbreviation "sublisteq" for special case

    "list_hembeq (op =)".

  - Theory Library/Sublist no longer provides "order" and "bot" type

    class instances for the prefix order (merely corresponding locale

    interpretations). The type class instances are now in theory

    Library/Prefix_Order.

  - The sublist relation of theory Library/Sublist_Order is now based

    on "Sublist.sublisteq".  Renamed lemmas accordingly:

      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff

      le_list_append_mono ~> Sublist.list_hembeq_append_mono

      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2

      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD

      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'

      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq

      le_list_drop_Cons ~> Sublist.sublisteq_Cons'

      le_list_drop_many ~> Sublist.sublisteq_drop_many

      le_list_filter_left ~> Sublist.sublisteq_filter_left

      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many

      le_list_rev_take_iff ~> Sublist.sublisteq_append

      le_list_same_length ~> Sublist.sublisteq_same_length

      le_list_take_many_iff ~> Sublist.sublisteq_append'

      less_eq_list.drop ~> less_eq_list_drop

      less_eq_list.induct ~> less_eq_list_induct

      not_le_list_length ~> Sublist.not_sublisteq_length

INCOMPATIBILITY.

* New theory Library/Countable_Set.

* Theory Library/Debug and Library/Parallel provide debugging and

parallel execution for code generated towards Isabelle/ML.

* Theory Library/FuncSet: Extended support for Pi and extensional and

introduce the extensional dependent function space "PiE". Replaced

extensional_funcset by an abbreviation, and renamed lemmas from

extensional_funcset to PiE as follows:

  extensional_empty  ~>  PiE_empty

  extensional_funcset_empty_domain  ~>  PiE_empty_domain

  extensional_funcset_empty_range  ~>  PiE_empty_range

  extensional_funcset_arb  ~>  PiE_arb

  extensional_funcset_mem  ~>  PiE_mem

  extensional_funcset_extend_domainI  ~>  PiE_fun_upd

  extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE

  extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq

  card_extensional_funcset  ~>  card_PiE

  finite_extensional_funcset  ~>  finite_PiE

INCOMPATIBILITY.

* Theory Library/FinFun: theory of almost everywhere constant

functions (supersedes the AFP entry "Code Generation for Functions as

Data").

* Theory Library/Phantom: generic phantom type to make a type

parameter appear in a constant's type.  This alternative to adding

TYPE('a) as another parameter avoids unnecessary closures in generated

code.

* Theory Library/RBT_Impl: efficient construction of red-black trees

from sorted associative lists. Merging two trees with rbt_union may

return a structurally different tree than before.  Potential

INCOMPATIBILITY.

* Theory Library/IArray: immutable arrays with code generation.

* Theory Library/Finite_Lattice: theory of finite lattices.

* HOL/Multivariate_Analysis: replaced

  "basis :: 'a::euclidean_space => nat => real"

  "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"

on euclidean spaces by using the inner product "_ \<bullet> _" with

vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by

"SUM i : Basis. f i * r i".

  With this change the following constants are also changed or removed:

    DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)

    a $$ i  ~>  inner a i  (where i : Basis)

    cart_base i  removed

    \<pi>, \<pi>'  removed

  Theorems about these constants where removed.

  Renamed lemmas:

    component_le_norm  ~>  Basis_le_norm

    euclidean_eq  ~>  euclidean_eq_iff

    differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart

    euclidean_simps  ~>  inner_simps

    independent_basis  ~>  independent_Basis

    span_basis  ~>  span_Basis

    in_span_basis  ~>  in_span_Basis

    norm_bound_component_le  ~>  norm_boound_Basis_le

    norm_bound_component_lt  ~>  norm_boound_Basis_lt

    component_le_infnorm  ~>  Basis_le_infnorm

INCOMPATIBILITY.

* HOL/Probability:

  - Added simproc "measurable" to automatically prove measurability.

  - Added induction rules for sigma sets with disjoint union

    (sigma_sets_induct_disjoint) and for Borel-measurable functions

    (borel_measurable_induct).

  - Added the Daniell-Kolmogorov theorem (the existence the limit of a

    projective family).

* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the

AFP entry "Ordinals_and_Cardinals").

* HOL/BNF: New (co)datatype package based on bounded natural functors

with support for mixed, nested recursion and interesting non-free

datatypes.

* HOL/Finite_Set and Relation: added new set and relation operations

expressed by Finite_Set.fold.

* New theory HOL/Library/RBT_Set: implementation of sets by red-black

trees for the code generator.

* HOL/Library/RBT and HOL/Library/Mapping have been converted to

Lifting/Transfer.

possible INCOMPATIBILITY.

* HOL/Set: renamed Set.project -> Set.filter

INCOMPATIBILITY.

*** Document preparation ***

* Dropped legacy antiquotations "term_style" and "thm_style", since

styles may be given as arguments to "term" and "thm" already.

Discontinued legacy styles "prem1" .. "prem19".

* Default LaTeX rendering for \<euro> is now based on eurosym package,

instead of slightly exotic babel/greek.

* Document variant NAME may use different LaTeX entry point

document/root_NAME.tex if that file exists, instead of the common

document/root.tex.

* Simplified custom document/build script, instead of old-style

document/IsaMakefile.  Minor INCOMPATIBILITY.

*** ML ***

* The default limit for maximum number of worker threads is now 8,

instead of 4, in correspondence to capabilities of contemporary

hardware and Poly/ML runtime system.

* Type Seq.results and related operations support embedded error

messages within lazy enumerations, and thus allow to provide

informative errors in the absence of any usable results.

* Renamed Position.str_of to Position.here to emphasize that this is a

formal device to inline positions into message text, but not

necessarily printing visible text.

*** System ***

* Advanced support for Isabelle sessions and build management, see

"system" manual for the chapter of that name, especially the "isabelle

build" tool and its examples.  The "isabelle mkroot" tool prepares

session root directories for use with "isabelle build", similar to

former "isabelle mkdir" for "isabelle usedir".  Note that this affects

document preparation as well.  INCOMPATIBILITY, isabelle usedir /

mkdir / make are rendered obsolete.

* Discontinued obsolete Isabelle/build script, it is superseded by the

regular isabelle build tool.  For example:

  isabelle build -s -b HOL

* Discontinued obsolete "isabelle makeall".

* Discontinued obsolete IsaMakefile and ROOT.ML files from the

Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that

provides some traditional targets that invoke "isabelle build".  Note

that this is inefficient!  Applications of Isabelle/HOL involving

"isabelle make" should be upgraded to use "isabelle build" directly.

* The "isabelle options" tool prints Isabelle system options, as

required for "isabelle build", for example.

* The "isabelle logo" tool produces EPS and PDF format simultaneously.

Minor INCOMPATIBILITY in command-line options.

* The "isabelle install" tool has now a simpler command-line.  Minor

INCOMPATIBILITY.

* The "isabelle components" tool helps to resolve add-on components

that are not bundled, or referenced from a bare-bones repository

version of Isabelle.

* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general

platform family: "linux", "macos", "windows".

* The ML system is configured as regular component, and no longer

picked up from some surrounding directory.  Potential INCOMPATIBILITY

for home-made settings.

* Improved ML runtime statistics (heap, threads, future tasks etc.).

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

without exception positions and advanced ML compiler/toplevel

configuration.

* Discontinued special treatment of Proof General -- no longer guess

PROOFGENERAL_HOME based on accidental file-system layout.  Minor

INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS

settings manually, or use a Proof General version that has been

bundled as Isabelle component.

New in Isabelle2012 (May 2012)

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

*** General ***

* Prover IDE (PIDE) improvements:

  - more robust Sledgehammer integration (as before the sledgehammer

    command-line needs to be typed into the source buffer)

  - markup for bound variables

  - markup for types of term variables (displayed as tooltips)

  - support for user-defined Isar commands within the running session

  - improved support for Unicode outside original 16bit range

    e.g. glyph for \<A> (thanks to jEdit 4.5.1)

* Forward declaration of outer syntax keywords within the theory

header -- minor INCOMPATIBILITY for user-defined commands.  Allow new

commands to be used in the same theory where defined.

* Auxiliary contexts indicate block structure for specifications with

additional parameters and assumptions.  Such unnamed contexts may be

nested within other targets, like 'theory', 'locale', 'class',

'instantiation' etc.  Results from the local context are generalized

accordingly and applied to the enclosing target context.  Example:

  context

    fixes x y z :: 'a

    assumes xy: "x = y" and yz: "y = z"

  begin

  lemma my_trans: "x = z" using xy yz by simp

  end

  thm my_trans

The most basic application is to factor-out context elements of

several fixes/assumes/shows theorem statements, e.g. see

~~/src/HOL/Isar_Examples/Group_Context.thy

Any other local theory specification element works within the "context

... begin ... end" block as well.

* Bundled declarations associate attributed fact expressions with a

given name in the context.  These may be later included in other

contexts.  This allows to manage context extensions casually, without

the logical dependencies of locales and locale interpretation.  See

commands 'bundle', 'include', 'including' etc. in the isar-ref manual.

* Commands 'lemmas' and 'theorems' allow local variables using 'for'

declaration, and results are standardized before being stored.  Thus

old-style "standard" after instantiation or composition of facts

becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of

indices of schematic variables.

* Rule attributes in local theory declarations (e.g. locale or class)

are now statically evaluated: the resulting theorem is stored instead

of the original expression.  INCOMPATIBILITY in rare situations, where

the historic accident of dynamic re-evaluation in interpretations

etc. was exploited.

* New tutorial "Programming and Proving in Isabelle/HOL"

("prog-prove").  It completely supersedes "A Tutorial Introduction to

Structured Isar Proofs" ("isar-overview"), which has been removed.  It

also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order

Logic" as the recommended beginners tutorial, but does not cover all

of the material of that old tutorial.

* Updated and extended reference manuals: "isar-ref",

"implementation", "system"; reduced remaining material in old "ref"

manual.

*** Pure ***

* Command 'definition' no longer exports the foundational "raw_def"

into the user context.  Minor INCOMPATIBILITY, may use the regular

"def" result with attribute "abs_def" to imitate the old version.

* Attribute "abs_def" turns an equation of the form "f x y == t" into

"f == %x y. t", which ensures that "simp" or "unfold" steps always

expand it.  This also works for object-logic equality.  (Formerly

undocumented feature.)

* Sort constraints are now propagated in simultaneous statements, just

like type constraints.  INCOMPATIBILITY in rare situations, where

distinct sorts used to be assigned accidentally.  For example:

  lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"

  lemma "P (x::'a)" and "Q (y::'a::bar)"

    -- "now uniform 'a::bar instead of default sort for first occurrence (!)"

* Rule composition via attribute "OF" (or ML functions OF/MRS) is more

tolerant against multiple unifiers, as long as the final result is

unique.  (As before, rules are composed in canonical right-to-left

order to accommodate newly introduced premises.)

* Renamed some inner syntax categories:

    num ~> num_token

    xnum ~> xnum_token

    xstr ~> str_token

Minor INCOMPATIBILITY.  Note that in practice "num_const" or

"num_position" etc. are mainly used instead (which also include

position information via constraints).

* Simplified configuration options for syntax ambiguity: see

"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

manual.  Minor INCOMPATIBILITY.

* Discontinued configuration option "syntax_positions": atomic terms

in parse trees are always annotated by position constraints.

* Old code generator for SML and its commands 'code_module',

'code_library', 'consts_code', 'types_code' have been discontinued.

Use commands of the generic code generator instead.  INCOMPATIBILITY.

* Redundant attribute "code_inline" has been discontinued. Use

"code_unfold" instead.  INCOMPATIBILITY.

* Dropped attribute "code_unfold_post" in favor of the its dual

"code_abbrev", which yields a common pattern in definitions like

  definition [code_abbrev]: "f = t"

INCOMPATIBILITY.

* Obsolete 'types' command has been discontinued.  Use 'type_synonym'

instead.  INCOMPATIBILITY.

* Discontinued old "prems" fact, which used to refer to the accidental

collection of foundational premises in the context (already marked as

legacy since Isabelle2011).

*** HOL ***

* Type 'a set is now a proper type constructor (just as before

Isabelle2008).  Definitions mem_def and Collect_def have disappeared.

Non-trivial INCOMPATIBILITY.  For developments keeping predicates and

sets separate, it is often sufficient to rephrase some set S that has

been accidentally used as predicates by "%x. x : S", and some

predicate P that has been accidentally used as set by "{x. P x}".

Corresponding proofs in a first step should be pruned from any

tinkering with former theorems mem_def and Collect_def as far as

possible.

For developments which deliberately mix predicates and sets, a

planning step is necessary to determine what should become a predicate

and what a set.  It can be helpful to carry out that step in

Isabelle2011-1 before jumping right into the current release.

* Code generation by default implements sets as container type rather

than predicates.  INCOMPATIBILITY.