NEWS

Int.thy: discontinued some legacy theorems

Isabelle NEWS -- history user-relevant changes
==============================================

New in this Isabelle version
----------------------------

*** HOL ***

* Theory Int: Discontinued many legacy theorems specific to type int.
  INCOMPATIBILITY, use the corresponding generic theorems instead.

  zminus_zminus ~> minus_minus
  zminus_0 ~> minus_zero
  zminus_zadd_distrib ~> minus_add_distrib
  zadd_commute ~> add_commute
  zadd_assoc ~> add_assoc
  zadd_left_commute ~> add_left_commute
  zmult_ac ~> mult_ac
  zadd_0 ~> add_0_left
  zadd_0_right ~> add_0_right
  zadd_zminus_inverse2 ~> left_minus
  zmult_zminus ~> mult_minus_left
  zmult_commute ~> mult_commute
  zmult_assoc ~> mult_assoc
  zadd_zmult_distrib ~> left_distrib
  zadd_zmult_distrib2 ~> right_distrib
  zdiff_zmult_distrib ~> left_diff_distrib
  zdiff_zmult_distrib2 ~> right_diff_distrib
  zmult_1 ~> mult_1_left
  zmult_1_right ~> mult_1_right
  zle_refl ~> order_refl
  zle_trans ~> order_trans
  zle_antisym ~> order_antisym
  zle_linear ~> linorder_linear
  zless_linear ~> linorder_less_linear
  zadd_left_mono ~> add_left_mono
  zadd_strict_right_mono ~> add_strict_right_mono
  zadd_zless_mono ~> add_less_le_mono
  int_0_less_1 ~> zero_less_one
  int_0_neq_1 ~> zero_neq_one
  zless_le ~> less_le
  zpower_zadd_distrib ~> power_add
  zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
  zero_le_zpower_abs ~> zero_le_power_abs



New in Isabelle2011-1 (October 2011)
------------------------------------

*** General ***

* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.

  - Management of multiple theory files directly from the editor
    buffer store -- bypassing the file-system (no requirement to save
    files for checking).

  - Markup of formal entities within the text buffer, with semantic
    highlighting, tooltips and hyperlinks to jump to defining source
    positions.

  - Improved text rendering, with sub/superscripts in the source
    buffer (including support for copy/paste wrt. output panel, HTML
    theory output and other non-Isabelle text boxes).

  - Refined scheduling of proof checking and printing of results,
    based on interactive editor view.  (Note: jEdit folding and
    narrowing allows to restrict buffer perspectives explicitly.)

  - Reduced CPU performance requirements, usable on machines with few
    cores.

  - Reduced memory requirements due to pruning of unused document
    versions (garbage collection).

See also ~~/src/Tools/jEdit/README.html for further information,
including some remaining limitations.

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

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

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

* Attribute "case_names" has been refined: the assumptions in each case
can be named now by following the case name with [name1 name2 ...].

* Isabelle/Isar reference manual has been updated and extended:
  - "Synopsis" provides a catalog of main Isar language concepts.
  - Formal references in syntax diagrams, via @{rail} antiquotation.
  - Updated material from classic "ref" manual, notably about
    "Classical Reasoner".


*** HOL ***

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

Removed redundant lemmas (the right hand side gives hints how to
replace them for (metis ...), or (simp only: ...) proofs):

  Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
  Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
  Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right
  Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right
  Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right
  Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right
  Inter_def ~> INF_def, image_def
  Union_def ~> SUP_def, image_def
  INT_eq ~> INF_def, and image_def
  UN_eq ~> SUP_def, and image_def
  INF_subset ~> INF_superset_mono [OF _ order_refl]

More consistent and comprehensive names:

  INTER_eq_Inter_image ~> INF_def
  UNION_eq_Union_image ~> SUP_def
  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.

* Renamed theory Complete_Lattice to Complete_Lattices.
INCOMPATIBILITY.

* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,
INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,
Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,
Sup_insert are now declared as [simp].  INCOMPATIBILITY.

* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,
compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,
sup_inf_absob, sup_left_idem are now declared as [simp].  Minor
INCOMPATIBILITY.

* Added syntactic classes "inf" and "sup" for the respective
constants.  INCOMPATIBILITY: Changes in the argument order of the
(mostly internal) locale predicates for some derived classes.

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

* Theory Archimedean_Field: floor now is defined as parameter of a
separate type class floor_ceiling.

* Theory Finite_Set: 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 characterization; interpretation proofs may need
adjustment.  INCOMPATIBILITY.

* Theory Limits: Type "'a net" has been renamed to "'a filter", in
accordance with standard mathematical terminology. INCOMPATIBILITY.

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

* Theory Complex_Main: Several redundant theorems have been removed or
replaced by more general versions. INCOMPATIBILITY.

  real_diff_def ~> minus_real_def
  real_divide_def ~> divide_real_def
  real_less_def ~> less_le
  real_abs_def ~> abs_real_def
  real_sgn_def ~> sgn_real_def
  real_mult_commute ~> mult_commute
  real_mult_assoc ~> mult_assoc
  real_mult_1 ~> mult_1_left
  real_add_mult_distrib ~> left_distrib
  real_zero_not_eq_one ~> zero_neq_one
  real_mult_inverse_left ~> left_inverse
  INVERSE_ZERO ~> inverse_zero
  real_le_refl ~> order_refl
  real_le_antisym ~> order_antisym
  real_le_trans ~> order_trans
  real_le_linear ~> linear
  real_le_eq_diff ~> le_iff_diff_le_0
  real_add_left_mono ~> add_left_mono
  real_mult_order ~> mult_pos_pos
  real_mult_less_mono2 ~> mult_strict_left_mono
  real_of_int_real_of_nat ~> real_of_int_of_nat_eq
  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
  real_sum_squared_expand ~> power2_sum
  exp_ln_eq ~> ln_unique
  expi_add ~> exp_add
  expi_zero ~> exp_zero
  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]
  LIMSEQ_Complex ~> tendsto_Complex
  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]

* Theory Complex_Main: The definition of infinite series was
generalized.  Now it is defined on the type class {topological_space,
comm_monoid_add}.  Hence it is useable also for extended real numbers.

* Theory Complex_Main: The complex exponential function "expi" is now
a type-constrained abbreviation for "exp :: complex => complex"; thus
several polymorphic lemmas about "exp" are now applicable to "expi".

* 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.  May be
    reactivated by the following theory command:

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

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

* New proof method "induction" that gives induction hypotheses the
name "IH", thus distinguishing them from further hypotheses that come
from rule induction.  The latter are still called "hyps".  Method
"induction" is a thin wrapper around "induct" and follows the same
syntax.

* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
still available as a legacy feature for some time.

* Nitpick:
  - Added "need" and "total_consts" options.
  - Reintroduced "show_skolems" option by popular demand.
  - Renamed attribute: nitpick_def ~> nitpick_unfold.
    INCOMPATIBILITY.

* Sledgehammer:
  - Use quasi-sound (and efficient) translations by default.
  - Added support for the following provers: E-ToFoF, LEO-II,
    Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.
  - Automatically preplay and minimize proofs before showing them if
    this can be done within reasonable time.
  - sledgehammer available_provers ~> sledgehammer supported_provers.
    INCOMPATIBILITY.
  - 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.

* Command '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.  Requires the Glasgow Haskell compiler
    with its installation location defined in the Isabelle settings
    environment as ISABELLE_GHC.
  - Removed quickcheck tester "SML" based on the SML code generator
    (formly in HOL/Library).

* Function package: discontinued option "tailrec".  INCOMPATIBILITY,
use 'partial_function' instead.

* Theory Library/Extended_Reals replaces now the positive extended
reals found in probability theory. This file is extended by
Multivariate_Analysis/Extended_Real_Limits.

* Theory Library/Old_Recdef: old 'recdef' package has been moved here,
from where it must be imported explicitly if it is really required.
INCOMPATIBILITY.

* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has
been moved here.  INCOMPATIBILITY.

* Theory Library/Saturated provides type of numbers with saturated
arithmetic.

* Theory Library/Product_Lattice defines a pointwise ordering for the
product type 'a * 'b, and provides instance proofs for various order
and lattice type classes.

* Theory Library/Countable now provides the "countable_datatype" proof
method for proving "countable" class instances for datatypes.

* Theory Library/Cset_Monad allows do notation for computable sets
(cset) via the generic monad ad-hoc overloading facility.

* Library: Theories of common data structures are split into theories
for implementation, an invariant-ensuring type, and connection to an
abstract type. INCOMPATIBILITY.

  - RBT is split into RBT and RBT_Mapping.
  - AssocList is split and renamed into AList and AList_Mapping.
  - DList is split into DList_Impl, DList, and DList_Cset.
  - Cset is split into Cset and List_Cset.

* Theory Library/Nat_Infinity has been renamed to
Library/Extended_Nat, with name changes of the following types and
constants:

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

* Session Multivariate_Analysis: The euclidean_space type class now
fixes a constant "Basis :: 'a set" consisting of the standard
orthonormal basis for the type. Users now have the option of
quantifying over this set instead of using the "basis" function, e.g.
"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".

* 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_sequentially ~> LIMSEQ_def
  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

* Session HOL-Probability:
  - Caratheodory's extension lemma is now proved for ring_of_sets.
  - Infinite products of probability measures are now available.
  - Sigma closure is independent, if the generator is independent
  - Use extended reals instead of positive extended
    reals. INCOMPATIBILITY.

* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

  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
  monofun_fun_fun ~> fun_belowD
  monofun_fun_arg ~> monofunE
  monofun_lub_fun ~> adm_monofun [THEN admD]
  cont_lub_fun ~> adm_cont [THEN admD]
  cont2cont_Rep_CFun ~> cont2cont_APP
  cont_Rep_CFun_app ~> cont_APP_app
  cont_Rep_CFun_app_app ~> cont_APP_app_app
  cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]
  cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]
  contlub_cfun ~> lub_APP [symmetric]
  contlub_LAM ~> lub_LAM [symmetric]
  thelubI ~> lub_eqI
  UU_I ~> bottomI
  lift_distinct1 ~> lift.distinct(1)
  lift_distinct2 ~> lift.distinct(2)
  Def_not_UU ~> lift.distinct(2)
  Def_inject ~> lift.inject
  below_UU_iff ~> below_bottom_iff
  eq_UU_iff ~> eq_bottom_iff


*** Document preparation ***

* Antiquotation @{rail} layouts railroad syntax diagrams, see also
isar-ref manual, both for description and actual application of the
same.

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

* Antiquotations: term style "isub" provides 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).

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

  \isabellestyle{it}  %preferred default
  {\isabellestylett @{text "typewriter stuff"}}

* Discontinued special treatment of hard tabulators.  Implicit
tab-width is now defined as 1.  Potential INCOMPATIBILITY for visual
layouts.


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


*** System ***

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

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

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

Together with YXML.string_of_body/parse_body and XML.Encode/Decode
this allows to pass structured values between ML and Scala.

* The IsabelleText fonts includes some further glyphs to support the
Prover IDE.  Potential INCOMPATIBILITY: users who happen to have
installed a local copy (which is normally *not* required) need to
delete or update it from ~~/lib/fonts/.



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.