Isabelle NEWS -- history of user-relevant changes

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

(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)

New in this Isabelle version

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

*** General ***

* Toplevel theorem statements have been simplified as follows:

  theorems             ~>  lemmas

  schematic_lemma      ~>  schematic_goal

  schematic_theorem    ~>  schematic_goal

  schematic_corollary  ~>  schematic_goal

Command-line tool "isabelle update_theorems" updates theory sources

accordingly.

* Toplevel theorem statement 'proposition' is another alias for

'theorem'.

* Syntax for formal comments "-- text" now also supports the symbolic

form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps

to update old sources.

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

* Completion of symbols via prefix of \<name> or \<^name> or \name is

always possible, independently of the language context. It is never

implicit: a popup will show up unconditionally.

* Improved scheduling for urgent print tasks (e.g. command state output,

interactive queries) wrt. long-running background tasks.

* IDE support for the source-level debugger of Poly/ML, to work with

Isabelle/ML and official Standard ML. Configuration option "ML_debugger"

and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',

'SML_file_no_debug' control compilation of sources with debugging

information. The Debugger panel allows to set breakpoints (via context

menu), step through stopped threads, evaluate local ML expressions etc.

At least one Debugger view needs to be active to have any effect on the

running ML program.

* The main Isabelle executable is managed as single-instance Desktop

application uniformly on all platforms: Linux, Windows, Mac OS X.

* The State panel manages explicit proof state output, with dynamic

auto-update according to cursor movement. Alternatively, the jEdit

action "isabelle.update-state" (shortcut S+ENTER) triggers manual

update.

* The Output panel no longer shows proof state output by default, to

avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or

enable option "editor_output_state".

* The text overview column (status of errors, warnings etc.) is updated

asynchronously, leading to much better editor reactivity. Moreover, the

full document node content is taken into account. The width of the

column is scaled according to the main text area font, for improved

visibility.

* The main text area no longer changes its color hue in outdated

situations. The text overview column takes over the role to indicate

unfinished edits in the PIDE pipeline. This avoids flashing text display

due to ad-hoc updates by auxiliary GUI components, such as the State

panel.

* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls

emphasized text style; the effect is visible in document output, not in

the editor.

* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,

instead of former C+e LEFT.

* New command-line tool "isabelle jedit_client" allows to connect to

already running Isabelle/jEdit process. This achieves the effect of

single-instance applications seen on common GUI desktops.

* The command-line tool "isabelle jedit" and the isabelle.Main

application wrapper threat the default $USER_HOME/Scratch.thy more

uniformly, and allow the dummy file argument ":" to open an empty buffer

instead.

* The default look-and-feel for Linux is the traditional "Metal", which

works better with GUI scaling for very high-resolution displays (e.g.

4K). Moreover, it is generally more robust than "Nimbus".

*** Document preparation ***

* There is a new short form for antiquotations with a single argument

that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and

\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.

\<^name> without following cartouche is equivalent to @{name}. The

standard Isabelle fonts provide glyphs to render important control

symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".

* Antiquotation @{theory_text} prints uninterpreted theory source text

(outer syntax with command keywords etc.). This may be used in the short

form \<^theory_text>\<open>...\<close>.   @{theory_text [display]} supports option "indent".

* @{verbatim [display]} supports option "indent".

* Antiquotation @{doc ENTRY} provides a reference to the given

documentation, with a hyperlink in the Prover IDE.

* Antiquotations @{command}, @{method}, @{attribute} print checked

entities of the Isar language.

* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with

corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using

standard LaTeX macros of the same names.

* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.

Consequently, \<open>...\<close> without any decoration prints literal quasi-formal

text. Command-line tool "isabelle update_cartouches -t" helps to update

old sources, by approximative patching of the content of string and

cartouche tokens seen in theory sources.

* The @{text} antiquotation now ignores the antiquotation option

"source". The given text content is output unconditionally, without any

surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the

argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial

or terminal spaces are ignored.

* HTML presentation uses the standard IsabelleText font and Unicode

rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former

print mode "HTML" loses its special meaning.

* Commands 'paragraph' and 'subparagraph' provide additional section

headings. Thus there are 6 levels of standard headings, as in HTML.

* Text is structured in paragraphs and nested lists, using notation that

is similar to Markdown. The control symbols for list items are as

follows:

  \<^item>  itemize

  \<^enum>  enumerate

  \<^descr>  description

* Command 'text_raw' has been clarified: input text is processed as in

'text' (with antiquotations and control symbols). The key difference is

the lack of the surrounding isabelle markup environment in output.

* Document antiquotations @{emph} and @{bold} output LaTeX source

recursively, adding appropriate text style markup. These may be used in

the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.

* Document antiquotation @{footnote} outputs LaTeX source recursively,

marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.

*** Isar ***

* Command 'obtain' binds term abbreviations (via 'is' patterns) in the

proof body as well, abstracted over relevant parameters.

* Improved type-inference for theorem statement 'obtains': separate

parameter scope for of each clause.

* Term abbreviations via 'is' patterns also work for schematic

statements: result is abstracted over unknowns.

* Local goals ('have', 'show', 'hence', 'thus') allow structured

rule statements like fixes/assumes/shows in theorem specifications, but

the notation is postfix with keywords 'if' (or 'when') and 'for'. For

example:

  have result: "C x y"

    if "A x" and "B y"

    for x :: 'a and y :: 'a

    <proof>

The local assumptions are bound to the name "that". The result is

exported from context of the statement as usual. The above roughly

corresponds to a raw proof block like this:

  {

    fix x :: 'a and y :: 'a

    assume that: "A x" "B y"

    have "C x y" <proof>

  }

  note result = this

The keyword 'when' may be used instead of 'if', to indicate 'presume'

instead of 'assume' above.

* Assumptions ('assume', 'presume') allow structured rule statements

using 'if' and 'for', similar to 'have' etc. above. For example:

  assume result: "C x y"

    if "A x" and "B y"

    for x :: 'a and y :: 'a

This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general

result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".

Vacuous quantification in assumptions is omitted, i.e. a for-context

only effects propositions according to actual use of variables. For

example:

  assume "A x" and "B y" for x and y

is equivalent to:

  assume "\<And>x. A x" and "\<And>y. B y"

* The meaning of 'show' with Pure rule statements has changed: premises

are treated in the sense of 'assume', instead of 'presume'. This means,

a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:

  show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

or:

  show "C x" if "A x" "B x" for x

Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

  show "C x" when "A x" "B x" for x

* New command 'supply' supports fact definitions during goal refinement

('apply' scripts).

* New command 'consider' states rules for generalized elimination and

case splitting. This is like a toplevel statement "theorem obtains" used

within a proof body; or like a multi-branch 'obtain' without activation

of the local context elements yet.

* Proof method "cases" allows to specify the rule as first entry of

chained facts.  This is particularly useful with 'consider':

  consider (a) A | (b) B | (c) C <proof>

  then have something

  proof cases

    case a

    then show ?thesis <proof>

  next

    case b

    then show ?thesis <proof>

  next

    case c

    then show ?thesis <proof>

  qed

* Command 'case' allows fact name and attribute specification like this:

  case a: (c xs)

  case a [attributes]: (c xs)

Facts that are introduced by invoking the case context are uniformly

qualified by "a"; the same name is used for the cumulative fact. The old

form "case (c xs) [attributes]" is no longer supported. Rare

INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,

and always put attributes in front.

* The standard proof method of commands 'proof' and '..' is now called

"standard" to make semantically clear what it is; the old name "default"

is still available as legacy for some time. Documentation now explains

'..' more accurately as "by standard" instead of "by rule".

* Command 'subgoal' allows to impose some structure on backward

refinements, to avoid proof scripts degenerating into long of 'apply'

sequences. Further explanations and examples are given in the isar-ref

manual.

* Proof method "goal_cases" turns the current subgoals into cases within

the context; the conclusion is bound to variable ?case in each case. For

example:

lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

proof goal_cases

  case (1 x)

  then show ?case using \<open>A x\<close> \<open>B x\<close> sorry

next

  case (2 y z)

  then show ?case using \<open>U y\<close> \<open>V z\<close> sorry

qed

lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

  and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

proof goal_cases

  case prems: 1

  then show ?case using prems sorry

next

  case prems: 2

  then show ?case using prems sorry

qed

* The undocumented feature of implicit cases goal1, goal2, goal3, etc.

is marked as legacy, and will be removed eventually. The proof method

"goals" achieves a similar effect within regular Isar; often it can be

done more adequately by other means (e.g. 'consider').

* Nesting of Isar goal structure has been clarified: the context after

the initial backwards refinement is retained for the whole proof, within

all its context sections (as indicated via 'next'). This is e.g.

relevant for 'using', 'including', 'supply':

  have "A \<and> A" if a: A for A

    supply [simp] = a

  proof

    show A by simp

  next

    show A by simp

  qed

* Method "sleep" succeeds after a real-time delay (in seconds). This is

occasionally useful for demonstration and testing purposes.

*** Pure ***

* Qualifiers in locale expressions default to mandatory ('!') regardless

of the command. Previously, for 'locale' and 'sublocale' the default was

optional ('?'). The old synatx '!' has been discontinued.

INCOMPATIBILITY, remove '!' and add '?' as required.

* Keyword 'rewrites' identifies rewrite morphisms in interpretation

commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.

* More gentle suppression of syntax along locale morphisms while

printing terms.  Previously 'abbreviation' and 'notation' declarations

would be suppressed for morphisms except term identity.  Now

'abbreviation' is also kept for morphims that only change the involved

parameters, and only 'notation' is suppressed.  This can be of great

help when working with complex locale hierarchies, because proof

states are displayed much more succinctly.  It also means that only

notation needs to be redeclared if desired, as illustrated by this

example:

  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)

  begin

    definition derived (infixl "\<odot>" 65) where ...

  end

  locale morphism =

    left: struct composition + right: struct composition'

    for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)

  begin

    notation right.derived ("\<odot>''")

  end

* Command 'sublocale' accepts rewrite definitions after keyword

'defines'.

* Command 'permanent_interpretation' is available in Pure, without

need to load a separate theory.  Keyword 'defines' identifies

rewrite definitions, keyword 'rewrites' identifies rewrite equations.

INCOMPATIBILITY.

* Command 'print_definitions' prints dependencies of definitional

specifications. This functionality used to be part of 'print_theory'.

* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`

as well, not just "by this" or "." as before.

* Configuration option rule_insts_schematic has been discontinued

(intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.

* Abbreviations in type classes now carry proper sort constraint.

Rare INCOMPATIBILITY in situations where the previous misbehaviour

has been exploited.

* Refinement of user-space type system in type classes: pseudo-local

operations behave more similar to abbreviations.  Potential

INCOMPATIBILITY in exotic situations.

*** HOL ***

* Combinator to represent case distinction on products is named "case_prod",

uniformly, discontinuing any input aliasses.  Very popular theorem aliasses

have been retained.

Consolidated facts:

  PairE ~> prod.exhaust

  Pair_eq ~> prod.inject

  pair_collapse ~> prod.collapse

  Pair_fst_snd_eq ~> prod_eq_iff

  split_twice ~> prod.case_distrib

  split_weak_cong ~> prod.case_cong_weak

  split_split ~> prod.split

  split_split_asm ~> prod.split_asm

  splitI ~> case_prodI

  splitD ~> case_prodD

  splitI2 ~> case_prodI2

  splitI2' ~> case_prodI2'

  splitE ~> case_prodE

  splitE' ~> case_prodE'

  split_pair ~> case_prod_Pair

  split_eta ~> case_prod_eta

  split_comp ~> case_prod_comp

  mem_splitI ~> mem_case_prodI

  mem_splitI2 ~> mem_case_prodI2

  mem_splitE ~> mem_case_prodE

  The_split ~> The_case_prod

  cond_split_eta ~> cond_case_prod_eta

  Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE

  Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI

  in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq

  Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD

  Collect_split_Grp_inD ~> Collect_case_prod_Grp_in

  Domain_Collect_split ~> Domain_Collect_case_prod

  Image_Collect_split ~> Image_Collect_case_prod

  Range_Collect_split ~> Range_Collect_case_prod

  Eps_split ~> Eps_case_prod

  Eps_split_eq ~> Eps_case_prod_eq

  split_rsp ~> case_prod_rsp

  curry_split ~> curry_case_prod

  split_curry ~> case_prod_curry

Changes in structure HOLogic:

  split_const ~> case_prod_const

  mk_split ~> mk_case_prod

  mk_psplits ~> mk_ptupleabs

  strip_psplits ~> strip_ptupleabs

INCOMPATIBILITY.

* Commands 'inductive' and 'inductive_set' work better when names for

intro rules are omitted: the "cases" and "induct" rules no longer

declare empty case_names, but no case_names at all. This allows to use

numbered cases in proofs, without requiring method "goal_cases".

* The 'typedef' command has been upgraded from a partially checked

"axiomatization", to a full definitional specification that takes the

global collection of overloaded constant / type definitions into

account. Type definitions with open dependencies on overloaded

definitions need to be specified as "typedef (overloaded)". This

provides extra robustness in theory construction. Rare INCOMPATIBILITY.

* Qualification of various formal entities in the libraries is done more

uniformly via "context begin qualified definition ... end" instead of

old-style "hide_const (open) ...". Consequently, both the defined

constant and its defining fact become qualified, e.g. Option.is_none and

Option.is_none_def. Occasional INCOMPATIBILITY in applications.

* The coercions to type 'real' have been reorganised. The function 'real'

is no longer overloaded, but has type 'nat => real' and abbreviates

of_nat for that type. Also 'real_of_int :: int => real' abbreviates

of_int for that type. Other overloaded instances of 'real' have been

replaced by 'real_of_ereal' and 'real_of_float'.

Consolidated facts (among others):

  real_of_nat_le_iff -> of_nat_le_iff

  real_of_nat_numeral of_nat_numeral

  real_of_int_zero of_int_0

  real_of_nat_zero of_nat_0

  real_of_one of_int_1

  real_of_int_add of_int_add

  real_of_nat_add of_nat_add

  real_of_int_diff of_int_diff

  real_of_nat_diff of_nat_diff

  floor_subtract floor_diff_of_int

  real_of_int_inject of_int_eq_iff

  real_of_int_gt_zero_cancel_iff of_int_0_less_iff

  real_of_int_ge_zero_cancel_iff of_int_0_le_iff

  real_of_nat_ge_zero of_nat_0_le_iff

  real_of_int_ceiling_ge le_of_int_ceiling

  ceiling_less_eq ceiling_less_iff

  ceiling_le_eq ceiling_le_iff

  less_floor_eq less_floor_iff

  floor_less_eq floor_less_iff

  floor_divide_eq_div floor_divide_of_int_eq

  real_of_int_zero_cancel of_nat_eq_0_iff

  ceiling_real_of_int ceiling_of_int

INCOMPATIBILITY.

* Some old and rarely used ASCII replacement syntax has been removed.

INCOMPATIBILITY, standard syntax with symbols should be used instead.

The subsequent commands help to reproduce the old forms, e.g. to

simplify porting old theories:

  type_notation Map.map  (infixr "~=>" 0)

  notation Map.map_comp  (infixl "o'_m" 55)

  type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

  notation FuncSet.funcset  (infixr "->" 60)

  notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)

  notation Omega_Words_Fun.conc (infixr "conc" 65)

  notation Preorder.equiv ("op ~~")

    and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

* The alternative notation "\<Colon>" for type and sort constraints has been

removed: in LaTeX document output it looks the same as "::".

INCOMPATIBILITY, use plain "::" instead.

* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has

been removed. INCOMPATIBILITY.

* Quickcheck setup for finite sets.

* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.

* Sledgehammer:

  - The MaSh relevance filter has been sped up.

  - Proof reconstruction has been improved, to minimize the incidence of

    cases where Sledgehammer gives a proof that does not work.

  - Auto Sledgehammer now minimizes and preplays the results.

  - Handle Vampire 4.0 proof output without raising exception.

  - Eliminated "MASH" environment variable. Use the "MaSh" option in

    Isabelle/jEdit instead. INCOMPATIBILITY.

  - Eliminated obsolete "blocking" option and related subcommands.

* Nitpick:

  - Fixed soundness bug in translation of "finite" predicate.

  - Fixed soundness bug in "destroy_constrs" optimization.

  - Removed "check_potential" and "check_genuine" options.

  - Eliminated obsolete "blocking" option.

* New (co)datatype package:

  - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF

    structure on the raw type to an abstract type defined using typedef.

  - Always generate "case_transfer" theorem.

  - Allow discriminators and selectors with the same name as the type

    being defined.

  - Avoid various internal name clashes (e.g., 'datatype f = f').

* Transfer:

  - new methods for interactive debugging of 'transfer' and

    'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',

    'transfer_prover_start' and 'transfer_prover_end'.

* Division on integers is bootstrapped directly from division on

naturals and uses generic numeral algorithm for computations.

Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes

former simprocs binary_int_div and binary_int_mod

* Tightened specification of class semiring_no_zero_divisors.  Slight

INCOMPATIBILITY.

* Class algebraic_semidom introduces common algebraic notions of

integral (semi)domains, particularly units.  Although

logically subsumed by fields, is is not a super class of these

in order not to burden fields with notions that are trivial there.

* Class normalization_semidom specifies canonical representants

for equivalence classes of associated elements in an integral

(semi)domain.  This formalizes associated elements as well.

* Abstract specification of gcd/lcm operations in classes semiring_gcd,

semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute

and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc

and gcd_int.assoc by gcd.assoc.

* Former constants Fields.divide (_ / _) and Divides.div (_ div _)

are logically unified to Rings.divide in syntactic type class

Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)

for field division is added later as abbreviation in class Fields.inverse.

INCOMPATIBILITY,  instantiations must refer to Rings.divide rather

than the former separate constants, hence infix syntax (_ / _) is usually

not available during instantiation.

* New cancellation simprocs for boolean algebras to cancel

complementary terms for sup and inf. For example, "sup x (sup y (- x))"

simplifies to "top". INCOMPATIBILITY.

* Library/Multiset:

  - Renamed multiset inclusion operators:

      < ~> <#

      \<subset> ~> \<subset>#

      <= ~> <=#

      \<le> ~> \<le>#

      \<subseteq> ~> \<subseteq>#

    INCOMPATIBILITY.

  - "'a multiset" is no longer an instance of the "order",

    "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",

    "semilattice_inf", and "semilattice_sup" type classes. The theorems

    previously provided by these type classes (directly or indirectly)

    are now available through the "subset_mset" interpretation

    (e.g. add_mono ~> subset_mset.add_mono).

    INCOMPATIBILITY.

  - Renamed conversions:

      multiset_of ~> mset

      multiset_of_set ~> mset_set

      set_of ~> set_mset

    INCOMPATIBILITY

  - Renamed lemmas:

      mset_le_def ~> subseteq_mset_def

      mset_less_def ~> subset_mset_def

      less_eq_multiset.rep_eq ~> subseteq_mset_def

    INCOMPATIBILITY

  - Removed lemmas generated by lift_definition:

    less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer

    less_eq_multiset_def

    INCOMPATIBILITY

* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt

fixpoint theorem for increasing functions in chain-complete partial

orders.

* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals),

Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light

* Multivariate_Analysis: Added topological concepts such as connected components,

homotopic paths and the inside or outside of a set.

* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'

command. Minor INCOMPATIBILITY, use 'function' instead.

* Inductive definitions ('inductive', 'coinductive', etc.) expose

low-level facts of the internal construction only if the option

"inductive_defs" is enabled. This refers to the internal predicate

definition and its monotonicity result. Rare INCOMPATIBILITY.

* Recursive function definitions ('fun', 'function', 'partial_function')

expose low-level facts of the internal construction only if the option

"function_defs" is enabled. Rare INCOMPATIBILITY.

* Data_Structures: new and growing session of standard data structures.

* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.

* Library/Omega_Words_Fun: Infinite words modeled as functions nat =>

'a.

* HOL-Statespace: command 'statespace' uses mandatory qualifier for

import of parent, as for general 'locale' expressions. INCOMPATIBILITY,

remove '!' and add '?' as required.

*** ML ***

* Isar proof methods are based on a slightly more general type

context_tactic, which allows to change the proof context dynamically

(e.g. to update cases) and indicate explicit Seq.Error results. Former

METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are

provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.

* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).

* The auxiliary module Pure/display.ML has been eliminated. Its

elementary thm print operations are now in Pure/more_thm.ML and thus

called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.

* Simproc programming interfaces have been simplified:

Simplifier.make_simproc and Simplifier.define_simproc supersede various

forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that

term patterns for the left-hand sides are specified with implicitly

fixed variables, like top-level theorem statements. INCOMPATIBILITY.

* Instantiation rules have been re-organized as follows:

  Thm.instantiate  (*low-level instantiation with named arguments*)

  Thm.instantiate' (*version with positional arguments*)

  Drule.infer_instantiate  (*instantiation with type inference*)

  Drule.infer_instantiate'  (*version with positional arguments*)

The LHS only requires variable specifications, instead of full terms.

Old cterm_instantiate is superseded by infer_instantiate.

INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.

* Old tactic shorthands atac, rtac, etac, dtac, ftac have been

discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.

instead (with proper context).

* Thm.instantiate (and derivatives) no longer require the LHS of the

instantiation to be certified: plain variables are given directly.

* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous

quasi-bound variables (like the Simplifier), instead of accidentally

named local fixes. This has the potential to improve stability of proof

tools, but can also cause INCOMPATIBILITY for tools that don't observe

the proof context discipline.

* The following combinators for low-level profiling of the ML runtime

system are available:

  profile_time          (*CPU time*)

  profile_time_thread   (*CPU time on this thread*)

  profile_allocations   (*overall heap allocations*)

*** System ***

* Global session timeout is multiplied by timeout_scale factor. This

allows to adjust large-scale tests (e.g. AFP) to overall hardware

performance.

* Property values in etc/symbols may contain spaces, if written with the

replacement character "␣" (Unicode point 0x2324).  For example:

    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono

* Command-line tool "isabelle update_then" expands old Isar command

conflations:

    hence  ~>  then have

    thus   ~>  then show

This syntax is more orthogonal and improves readability and

maintainability of proofs.

* Poly/ML default platform architecture may be changed from 32bit to

64bit via system option ML_system_64. A system restart (and rebuild)

is required after change.

* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which

both allow larger heap space than former x86-cygwin.

* Java runtime environment for x86_64-windows allows to use larger heap

space.

* Java runtime options are determined separately for 32bit vs. 64bit

platforms as follows.

  - Isabelle desktop application: platform-specific files that are

    associated with the main app bundle

  - isabelle jedit: settings

    JEDIT_JAVA_SYSTEM_OPTIONS

    JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

  - isabelle build: settings

    ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

* Bash shell function "jvmpath" has been renamed to "platform_path": it

is relevant both for Poly/ML and JVM processes.

* Heap images are 10-15% smaller due to less wasteful persistent theory

content (using ML type theory_id instead of theory);

New in Isabelle2015 (May 2015)

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

*** General ***

* Local theory specification commands may have a 'private' or

'qualified' modifier to restrict name space accesses to the local scope,

as provided by some "context begin ... end" block. For example:

  context

  begin

  private definition ...

  private lemma ...

  qualified definition ...

  qualified lemma ...

  lemma ...

  theorem ...

  end

* Command 'experiment' opens an anonymous locale context with private

naming policy.

* Command 'notepad' requires proper nesting of begin/end and its proof

structure in the body: 'oops' is no longer supported here. Minor

INCOMPATIBILITY, use 'sorry' instead.

* Command 'named_theorems' declares a dynamic fact within the context,

together with an attribute to maintain the content incrementally. This

supersedes functor Named_Thms in Isabelle/ML, but with a subtle change

of semantics due to external visual order vs. internal reverse order.

* 'find_theorems': search patterns which are abstractions are

schematically expanded before search. Search results match the naive

expectation more closely, particularly wrt. abbreviations.

INCOMPATIBILITY.

* Commands 'method_setup' and 'attribute_setup' now work within a local

theory context.

* Outer syntax commands are managed authentically within the theory

context, without implicit global state. Potential for accidental

INCOMPATIBILITY, make sure that required theories are really imported.

* Historical command-line terminator ";" is no longer accepted (and

already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle

update_semicolons" to remove obsolete semicolons from old theory

sources.

* Structural composition of proof methods (meth1; meth2) in Isar

corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

* The Eisbach proof method language allows to define new proof methods

by combining existing ones with their usual syntax. The "match" proof

method provides basic fact/term matching in addition to

premise/conclusion matching through Subgoal.focus, and binds fact names

from matches as well as term patterns within matches. The Isabelle

documentation provides an entry "eisbach" for the Eisbach User Manual.

Sources and various examples are in ~~/src/HOL/Eisbach/.

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

* Improved folding mode "isabelle" based on Isar syntax. Alternatively,

the "sidekick" mode may be used for document structure.

* Extended bracket matching based on Isar language structure. System

option jedit_structure_limit determines maximum number of lines to scan

in the buffer.

* Support for BibTeX files: context menu, context-sensitive token

marker, SideKick parser.

* Document antiquotation @{cite} provides formal markup, which is

interpreted semi-formally based on .bib files that happen to be open in

the editor (hyperlinks, completion etc.).

* Less waste of vertical space via negative line spacing (see Global

Options / Text Area).

* Improved graphview panel with optional output of PNG or PDF, for

display of 'thy_deps', 'class_deps' etc.

* The commands 'thy_deps' and 'class_deps' allow optional bounds to

restrict the visualized hierarchy.

* Improved scheduling for asynchronous print commands (e.g. provers

managed by the Sledgehammer panel) wrt. ongoing document processing.

*** Document preparation ***

* Document markup commands 'chapter', 'section', 'subsection',

'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any

context, even before the initial 'theory' command. Obsolete proof

commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been

discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'

instead. The old 'header' command is still retained for some time, but

should be replaced by 'chapter', 'section' etc. (using "isabelle

update_header"). Minor INCOMPATIBILITY.

* Official support for "tt" style variants, via \isatt{...} or

\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or

verbatim environment of LaTeX is no longer used. This allows @{ML} etc.

as argument to other macros (such as footnotes).

* Document antiquotation @{verbatim} prints ASCII text literally in "tt"

style.

* Discontinued obsolete option "document_graph": session_graph.pdf is

produced unconditionally for HTML browser_info and PDF-LaTeX document.

* Diagnostic commands and document markup commands within a proof do not

affect the command tag for output. Thus commands like 'thm' are subject

to proof document structure, and no longer "stick out" accidentally.

Commands 'text' and 'txt' merely differ in the LaTeX style, not their

tags. Potential INCOMPATIBILITY in exotic situations.

* System option "pretty_margin" is superseded by "thy_output_margin",

which is also accessible via document antiquotation option "margin".

Only the margin for document output may be changed, but not the global

pretty printing: that is 76 for plain console output, and adapted

dynamically in GUI front-ends. Implementations of document

antiquotations need to observe the margin explicitly according to

Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

* Specification of 'document_files' in the session ROOT file is

mandatory for document preparation. The legacy mode with implicit

copying of the document/ directory is no longer supported. Minor

INCOMPATIBILITY.

*** Pure ***

* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"

etc.) allow an optional context of local variables ('for' declaration):

these variables become schematic in the instantiated theorem; this

behaviour is analogous to 'for' in attributes "where" and "of".

Configuration option rule_insts_schematic (default false) controls use

of schematic variables outside the context. Minor INCOMPATIBILITY,

declare rule_insts_schematic = true temporarily and update to use local

variable declarations or dummy patterns instead.

* Explicit instantiation via attributes "where", "of", and proof methods

"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns

("_") that stand for anonymous local variables.

* Generated schematic variables in standard format of exported facts are

incremented to avoid material in the proof context. Rare

INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

different index.

* Lexical separation of signed and unsigned numerals: categories "num"

and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence

of numeral signs, particularly in expressions involving infix syntax

like "(- 1) ^ n".

* Old inner token category "xnum" has been discontinued.  Potential

INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"

token category instead.

*** HOL ***

* New (co)datatype package:

  - The 'datatype_new' command has been renamed 'datatype'. The old

    command of that name is now called 'old_datatype' and is provided

    by "~~/src/HOL/Library/Old_Datatype.thy". See

    'isabelle doc datatypes' for information on porting.

    INCOMPATIBILITY.

  - Renamed theorems:

      disc_corec ~> corec_disc

      disc_corec_iff ~> corec_disc_iff

      disc_exclude ~> distinct_disc

      disc_exhaust ~> exhaust_disc

      disc_map_iff ~> map_disc_iff

      sel_corec ~> corec_sel

      sel_exhaust ~> exhaust_sel

      sel_map ~> map_sel

      sel_set ~> set_sel

      sel_split ~> split_sel

      sel_split_asm ~> split_sel_asm

      strong_coinduct ~> coinduct_strong

      weak_case_cong ~> case_cong_weak

    INCOMPATIBILITY.

  - The "no_code" option to "free_constructors", "datatype_new", and

    "codatatype" has been renamed "plugins del: code".

    INCOMPATIBILITY.

  - The rules "set_empty" have been removed. They are easy

    consequences of other set rules "by auto".

    INCOMPATIBILITY.

  - The rule "set_cases" is now registered with the "[cases set]"

    attribute. This can influence the behavior of the "cases" proof

    method when more than one case rule is applicable (e.g., an

    assumption is of the form "w : set ws" and the method "cases w"

    is invoked). The solution is to specify the case rule explicitly

    (e.g. "cases w rule: widget.exhaust").

    INCOMPATIBILITY.

  - Renamed theories:

      BNF_Comp ~> BNF_Composition

      BNF_FP_Base ~> BNF_Fixpoint_Base

      BNF_GFP ~> BNF_Greatest_Fixpoint

      BNF_LFP ~> BNF_Least_Fixpoint

      BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions

      Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions

    INCOMPATIBILITY.

  - Lifting and Transfer setup for basic HOL types sum and prod (also

    option) is now performed by the BNF package. Theories Lifting_Sum,

    Lifting_Product and Lifting_Option from Main became obsolete and

    were removed. Changed definitions of the relators rel_prod and

    rel_sum (using inductive).

    INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead

    of rel_prod_def and rel_sum_def.

    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names

    changed (e.g. map_prod_transfer ~> prod.map_transfer).

  - Parametricity theorems for map functions, relators, set functions,

    constructors, case combinators, discriminators, selectors and

    (co)recursors are automatically proved and registered as transfer

    rules.

* Old datatype package:

  - The old 'datatype' command has been renamed 'old_datatype', and

    'rep_datatype' has been renamed 'old_rep_datatype'. They are

    provided by "~~/src/HOL/Library/Old_Datatype.thy". See

    'isabelle doc datatypes' for information on porting.

    INCOMPATIBILITY.

  - Renamed theorems:

      weak_case_cong ~> case_cong_weak

    INCOMPATIBILITY.

  - Renamed theory:

      ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy

    INCOMPATIBILITY.

* Nitpick:

  - Fixed soundness bug related to the strict and non-strict subset

    operations.

* Sledgehammer:

  - CVC4 is now included with Isabelle instead of CVC3 and run by

    default.

  - Z3 is now always enabled by default, now that it is fully open

    source. The "z3_non_commercial" option is discontinued.

  - Minimization is now always enabled by default.

    Removed sub-command:

      min

  - Proof reconstruction, both one-liners and Isar, has been

    dramatically improved.

  - Improved support for CVC4 and veriT.

* Old and new SMT modules:

  - The old 'smt' method has been renamed 'old_smt' and moved to

    'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,

    until applications have been ported to use the new 'smt' method. For

    the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must

    be installed, and the environment variable "OLD_Z3_SOLVER" must

    point to it.

    INCOMPATIBILITY.

  - The 'smt2' method has been renamed 'smt'.

    INCOMPATIBILITY.

  - New option 'smt_reconstruction_step_timeout' to limit the

    reconstruction time of Z3 proof steps in the new 'smt' method.