Isabelle NEWS -- history of user-relevant changes

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

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

New in Isabelle2018 (August 2018)

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

*** General ***

* Session-qualified theory names are mandatory: it is no longer possible

to refer to unqualified theories from the parent session.

INCOMPATIBILITY for old developments that have not been updated to

Isabelle2017 yet (using the "isabelle imports" tool).

* Only the most fundamental theory names are global, usually the entry

points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,

FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for

formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".

* Marginal comments need to be written exclusively in the new-style form

"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer

supported. INCOMPATIBILITY, use the command-line tool "isabelle

update_comments" to update existing theory files.

* Old-style inner comments (* ... *) within the term language are legacy

and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"

instead.

* The "op <infix-op>" syntax for infix operators has been replaced by

"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to

be a space between the "*" and the corresponding parenthesis.

INCOMPATIBILITY.

There is an Isabelle tool "update_op" that converts theory and ML files

to the new syntax. Because it is based on regular expression matching,

the result may need a bit of manual postprocessing. Invoking "isabelle

update_op" converts all files in the current directory (recursively).

In case you want to exclude conversion of ML files (because the tool

frequently also converts ML's "op" syntax), use option "-m".

* Theory header 'abbrevs' specifications need to be separated by 'and'.

INCOMPATIBILITY.

* Command 'external_file' declares the formal dependency on the given

file name, such that the Isabelle build process knows about it, but

without specific Prover IDE management.

* Session ROOT entries no longer allow specification of 'files'. Rare

INCOMPATIBILITY, use command 'external_file' within a proper theory

context.

* Session root directories may be specified multiple times: each

accessible ROOT file is processed only once. This facilitates

specification of $ISABELLE_HOME_USER/ROOTS or command-line options like

-d or -D for "isabelle build" and "isabelle jedit". Example:

  isabelle build -D '~~/src/ZF'

* The command 'display_drafts' has been discontinued. INCOMPATIBILITY,

use action "isabelle.draft" (or "print") in Isabelle/jEdit instead.

* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit

Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen"

U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML

output.

*** Isabelle/jEdit Prover IDE ***

* The command-line tool "isabelle jedit" provides more flexible options

for session management:

  - option -R builds an auxiliary logic image with all theories from

    other sessions that are not already present in its parent

  - option -S is like -R, with a focus on the selected session and its

    descendants (this reduces startup time for big projects like AFP)

  - option -A specifies an alternative ancestor session for options -R

    and -S

  Examples:

    isabelle jedit -R HOL-Number_Theory

    isabelle jedit -R HOL-Number_Theory -A HOL

    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL

    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis

* PIDE markup for session ROOT files: allows to complete session names,

follow links to theories and document files etc.

* Completion supports theory header imports, using theory base name.

E.g. "Prob" may be completed to "HOL-Probability.Probability".

* Named control symbols (without special Unicode rendering) are shown as

bold-italic keyword. This is particularly useful for the short form of

antiquotations with control symbol: \<^name>\<open>argument\<close>. The action

"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1

arguments into this format.

* Completion provides templates for named symbols with arguments,

e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".

* Slightly more parallel checking, notably for high priority print

functions (e.g. State output).

* The view title is set dynamically, according to the Isabelle

distribution and the logic session name. The user can override this via

set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml).

* System options "spell_checker_include" and "spell_checker_exclude"

supersede former "spell_checker_elements" to determine regions of text

that are subject to spell-checking. Minor INCOMPATIBILITY.

* Action "isabelle.preview" is able to present more file formats,

notably bibtex database files and ML files.

* Action "isabelle.draft" is similar to "isabelle.preview", but shows a

plain-text document draft. Both are available via the menu "Plugins /

Isabelle".

* Bibtex database files (.bib) are semantically checked.

* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle

is only used if there is no conflict with existing Unicode sequences in

the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle

symbols remain in literal \<symbol> form. This avoids accidental loss of

Unicode content when saving the file.

* Update to jedit-5.5.0, the latest release.

*** Isabelle/VSCode Prover IDE ***

* HTML preview of theories and other file-formats similar to

Isabelle/jEdit.

*** Document preparation ***

* Formal comments work uniformly in outer syntax, inner syntax (term

language), Isabelle/ML and some other embedded languages of Isabelle.

See also "Document comments" in the isar-ref manual. The following forms

are supported:

  - marginal text comment: \<comment> \<open>\<dots>\<close>

  - canceled source: \<^cancel>\<open>\<dots>\<close>

  - raw LaTeX: \<^latex>\<open>\<dots>\<close>

* Outside of the inner theory body, the default presentation context is

theory Pure. Thus elementary antiquotations may be used in markup

commands (e.g. 'chapter', 'section', 'text') and formal comments.

* System option "document_tags" specifies a default for otherwise

untagged commands. This is occasionally useful to control the global

visibility of commands via session options (e.g. in ROOT).

* Document markup commands ('section', 'text' etc.) are implicitly

tagged as "document" and visible by default. This avoids the application

of option "document_tags" to these commands.

* Isabelle names are mangled into LaTeX macro names to allow the full

identifier syntax with underscore, prime, digits. This is relevant for

antiquotations in control symbol notation, e.g. \<^const_name> becomes

\isactrlconstUNDERSCOREname.

* Document preparation with skip_proofs option now preserves the content

more accurately: only terminal proof steps ('by' etc.) are skipped.

* Document antiquotation @{session name} checks and prints the given

session name verbatim.

* Document antiquotation @{cite} now checks the given Bibtex entries

against the Bibtex database files -- only in batch-mode session builds.

* Command-line tool "isabelle document" has been re-implemented in

Isabelle/Scala, with simplified arguments and explicit errors from the

latex and bibtex process. Minor INCOMPATIBILITY.

* Session ROOT entry: empty 'document_files' means there is no document

for this session. There is no need to specify options [document = false]

anymore.

*** Isar ***

* Command 'interpret' no longer exposes resulting theorems as literal

facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This

improves modularity of proofs and scalability of locale interpretation.

Rare INCOMPATIBILITY, need to refer to explicitly named facts instead

(e.g. use 'find_theorems' or 'try' to figure this out).

* The old 'def' command has been discontinued (legacy since

Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with

object-logic equality or equivalence.

* Rewrites clauses (keyword 'rewrites') were moved into the locale

expression syntax, where they are part of locale instances. In

interpretation commands rewrites clauses now need to occur before 'for'

and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to

rewriting may need to be pulled up into the surrounding theory.

* For 'rewrites' clauses, if activating a locale instance fails, fall

back to reading the clause first. This helps avoid qualification of

locale instances where the qualifier's sole purpose is avoiding

duplicate constant declarations.

* Proof method 'simp' now supports a new modifier 'flip:' followed by a list

of theorems. Each of these theorems is removed from the simpset

(without warning if it is not there) and the symmetric version of the theorem

(i.e. lhs and rhs exchanged) is added to the simpset.

For 'auto' and friends the modifier is "simp flip:".

*** Pure ***

* The inner syntax category "sort" now includes notation "_" for the

dummy sort: it is effectively ignored in type-inference.

*** HOL ***

* Clarified relationship of characters, strings and code generation:

  - Type "char" is now a proper datatype of 8-bit values.

  - Conversions "nat_of_char" and "char_of_nat" are gone; use more

    general conversions "of_char" and "char_of" with suitable type

    constraints instead.

  - The zero character is just written "CHR 0x00", not "0" any longer.

  - Type "String.literal" (for code generation) is now isomorphic to

    lists of 7-bit (ASCII) values; concrete values can be written as

    "STR ''...''" for sequences of printable characters and "STR 0x..."

    for one single ASCII code point given as hexadecimal numeral.

  - Type "String.literal" supports concatenation "... + ..." for all

    standard target languages.

  - Theory HOL-Library.Code_Char is gone; study the explanations

    concerning "String.literal" in the tutorial on code generation to

    get an idea how target-language string literals can be converted to

    HOL string values and vice versa.

  - Session Imperative-HOL: operation "raise" directly takes a value of

    type "String.literal" as argument, not type "string".

INCOMPATIBILITY.

* Code generation: Code generation takes an explicit option

"case_insensitive" to accomodate case-insensitive file systems.

* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit.

* New, more general, axiomatization of complete_distrib_lattice. The

former axioms:

  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"

are replaced by:

  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"

The instantiations of sets and functions as complete_distrib_lattice are

moved to Hilbert_Choice.thy because their proofs need the Hilbert choice

operator. The dual of this property is also proved in theory

HOL.Hilbert_Choice.

* New syntax for the minimum/maximum of a function over a finite set:

MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX.

* Clarifed theorem names:

  Min.antimono ~> Min.subset_imp

  Max.antimono ~> Max.subset_imp

Minor INCOMPATIBILITY.

* SMT module:

  - The 'smt_oracle' option is now necessary when using the 'smt' method

    with a solver other than Z3. INCOMPATIBILITY.

  - The encoding to first-order logic is now more complete in the

    presence of higher-order quantifiers. An 'smt_explicit_application'

    option has been added to control this. INCOMPATIBILITY.

* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to

sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on

interpretation of abstract locales. INCOMPATIBILITY.

* Predicate coprime is now a real definition, not a mere abbreviation.

INCOMPATIBILITY.

* Predicate pairwise_coprime abolished, use "pairwise coprime" instead.

INCOMPATIBILITY.

* The relator rel_filter on filters has been strengthened to its

canonical categorical definition with better properties.

INCOMPATIBILITY.

* Generalized linear algebra involving linear, span, dependent, dim

from type class real_vector to locales module and vector_space.

Renamed:

  span_inc ~> span_superset

  span_superset ~> span_base

  span_eq ~> span_eq_iff

INCOMPATIBILITY.

* Class linordered_semiring_1 covers zero_less_one also, ruling out

pathologic instances. Minor INCOMPATIBILITY.

* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every

element in a list to all following elements, not just the next one.

* Theory HOL.List syntax:

  - filter-syntax "[x <- xs. P]" is no longer output syntax, but only

    input syntax

  - list comprehension syntax now supports tuple patterns in "pat <- xs"

* Theory Map: "empty" must now be qualified as "Map.empty".

* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.

* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid

clash with fact mod_mult_self4 (on more generic semirings).

INCOMPATIBILITY.

* Eliminated some theorem aliasses:

  even_times_iff ~> even_mult_iff

  mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1

  even_of_nat ~> even_int_iff

INCOMPATIBILITY.

* Eliminated some theorem duplicate variations:

  - dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0

  - mod_Suc_eq_Suc_mod can be replaced by mod_Suc

  - mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps

  - mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def

  - the witness of mod_eqD can be given directly as "_ div _"

INCOMPATIBILITY.

* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no

longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding

"elim!: dvd" to classical proof methods in most situations restores

broken proofs.

* Theory HOL-Library.Conditional_Parametricity provides command

'parametric_constant' for proving parametricity of non-recursive

definitions. For constants that are not fully parametric the command

will infer conditions on relations (e.g., bi_unique, bi_total, or type

class conditions such as "respects 0") sufficient for parametricity. See

theory HOL-ex.Conditional_Parametricity_Examples for some examples.

* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code

generator to generate code for algebraic types with lazy evaluation

semantics even in call-by-value target languages. See theory

HOL-Codegenerator_Test.Code_Lazy_Test for some examples.

* Theory HOL-Library.Landau_Symbols has been moved here from AFP.

* Theory HOL-Library.Old_Datatype no longer provides the legacy command

'old_datatype'. INCOMPATIBILITY.

* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide

instances of rat, real, complex as factorial rings etc. Import

HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.

INCOMPATIBILITY.

* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new

infix/prefix notation.

* Session HOL-Algebra: Revamped with much new material.

The set of isomorphisms between two groups is now denoted iso rather than iso_set.

INCOMPATIBILITY.

* Session HOL-Analysis: infinite products, Moebius functions, the

Riemann mapping theorem, the Vitali covering theorem,

change-of-variables results for integration and measures.

*** ML ***

* Operation Export.export emits theory exports (arbitrary blobs), which

are stored persistently in the session build database.

* Command 'ML_export' exports ML toplevel bindings to the global

bootstrap environment of the ML process. This allows ML evaluation

without a formal theory context, e.g. in command-line tools like

"isabelle process".

*** System ***

* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no

longer supported.

* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform

support has been discontinued.

* Java runtime is for x86_64 only. Corresponding Isabelle settings have

been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS,

instead of former 32/64 variants. INCOMPATIBILITY.

* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be

phased out due to unclear preference of 32bit vs. 64bit architecture.

Explicit GNU bash expressions are now preferred, for example (with

quotes):

  #Posix executables (Unix or Cygwin), with preference for 64bit

  "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"

  #native Windows or Unix executables, with preference for 64bit

  "${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}"

  #native Windows (32bit) or Unix executables (preference for 64bit)

  "${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}"

* Command-line tool "isabelle build" supports new options:

  - option -B NAME: include session NAME and all descendants

  - option -S: only observe changes of sources, not heap images

  - option -f: forces a fresh build

* Command-line tool "isabelle build" takes "condition" options with the

corresponding environment values into account, when determining the

up-to-date status of a session.

* The command-line tool "dump" dumps information from the cumulative

PIDE session database: many sessions may be loaded into a given logic

image, results from all loaded theories are written to the output

directory.

* Command-line tool "isabelle imports -I" also reports actual session

imports. This helps to minimize the session dependency graph.

* The command-line tool "export" and 'export_files' in session ROOT

entries retrieve theory exports from the session build database.

* The command-line tools "isabelle server" and "isabelle client" provide

access to the Isabelle Server: it supports responsive session management

and concurrent use of theories, based on Isabelle/PIDE infrastructure.

See also the "system" manual.

* The command-line tool "isabelle update_comments" normalizes formal

comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to

approximate the appearance in document output). This is more specific

than former "isabelle update_cartouches -c": the latter tool option has

been discontinued.

* The command-line tool "isabelle mkroot" now always produces a document

outline: its options have been adapted accordingly. INCOMPATIBILITY.

* The command-line tool "isabelle mkroot -I" initializes a Mercurial

repository for the generated session files.

* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:

heap images and session databases are always stored in

$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or

$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or

"isabelle jedit -s" or "isabelle build -s").

* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific

options for improved error reporting. Potential INCOMPATIBILITY with

unusual LaTeX installations, may have to adapt these settings.

* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE

markup for identifier bindings. It now uses The GNU Multiple Precision

Arithmetic Library (libgmp) on all platforms, notably Mac OS X with

32/64 bit.

New in Isabelle2017 (October 2017)

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

*** General ***

* Experimental support for Visual Studio Code (VSCode) as alternative

Isabelle/PIDE front-end, see also

https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017

VSCode is a new type of application that continues the concepts of

"programmer's editor" and "integrated development environment" towards

fully semantic editing and debugging -- in a relatively light-weight

manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.

Technically, VSCode is based on the Electron application framework

(Node.js + Chromium browser + V8), which is implemented in JavaScript

and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala

modules around a Language Server implementation.

* Theory names are qualified by the session name that they belong to.

This affects imports, but not the theory name space prefix (which is

just the theory base name as before).

In order to import theories from other sessions, the ROOT file format

provides a new 'sessions' keyword. In contrast, a theory that is

imported in the old-fashioned manner via an explicit file-system path

belongs to the current session, and might cause theory name conflicts

later on. Theories that are imported from other sessions are excluded

from the current session document. The command-line tool "isabelle

imports" helps to update theory imports.

* The main theory entry points for some non-HOL sessions have changed,

to avoid confusion with the global name "Main" of the session HOL. This

leads to the follow renamings:

  CTT/Main.thy    ~>  CTT/CTT.thy

  ZF/Main.thy     ~>  ZF/ZF.thy

  ZF/Main_ZF.thy  ~>  ZF/ZF.thy

  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy

  ZF/ZF.thy       ~>  ZF/ZF_Base.thy

INCOMPATIBILITY.

* Commands 'alias' and 'type_alias' introduce aliases for constants and

type constructors, respectively. This allows adhoc changes to name-space

accesses within global or local theory contexts, e.g. within a 'bundle'.

* Document antiquotations @{prf} and @{full_prf} output proof terms

(again) in the same way as commands 'prf' and 'full_prf'.

* Computations generated by the code generator can be embedded directly

into ML, alongside with @{code} antiquotations, using the following

antiquotations:

  @{computation ... terms: ... datatypes: ...} :

    ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a

  @{computation_conv ... terms: ... datatypes: ...} :

    (Proof.context -> 'ml -> conv) -> Proof.context -> conv

  @{computation_check terms: ... datatypes: ...} : Proof.context -> conv

See src/HOL/ex/Computations.thy,

src/HOL/Decision_Procs/Commutative_Ring.thy and

src/HOL/Decision_Procs/Reflective_Field.thy for examples and the

tutorial on code generation.

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

* Session-qualified theory imports allow the Prover IDE to process

arbitrary theory hierarchies independently of the underlying logic

session image (e.g. option "isabelle jedit -l"), but the directory

structure needs to be known in advance (e.g. option "isabelle jedit -d"

or a line in the file $ISABELLE_HOME_USER/ROOTS).

* The PIDE document model maintains file content independently of the

status of jEdit editor buffers. Reloading jEdit buffers no longer causes

changes of formal document content. Theory dependencies are always

resolved internally, without the need for corresponding editor buffers.

The system option "jedit_auto_load" has been discontinued: it is

effectively always enabled.

* The Theories dockable provides a "Purge" button, in order to restrict

the document model to theories that are required for open editor

buffers.

* The Theories dockable indicates the overall status of checking of each

entry. When all forked tasks of a theory are finished, the border is

painted with thick lines; remaining errors in this situation are

represented by a different border color.

* Automatic indentation is more careful to avoid redundant spaces in

intermediate situations. Keywords are indented after input (via typed

characters or completion); see also option "jedit_indent_input".

* Action "isabelle.preview" opens an HTML preview of the current theory

document in the default web browser.

* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT

entry of the specified logic session in the editor, while its parent is

used for formal checking.

* The main Isabelle/jEdit plugin may be restarted manually (using the

jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains

enabled at all times.

* Update to current jedit-5.4.0.

*** Pure ***

* Deleting the last code equations for a particular function using

[code del] results in function with no equations (runtime abort) rather

than an unimplemented function (generation time abort). Use explicit

[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.

* Proper concept of code declarations in code.ML:

  - Regular code declarations act only on the global theory level, being

    ignored with warnings if syntactically malformed.

  - Explicitly global code declarations yield errors if syntactically

    malformed.

  - Default code declarations are silently ignored if syntactically

    malformed.

Minor INCOMPATIBILITY.

* Clarified and standardized internal data bookkeeping of code

declarations: history of serials allows to track potentially

non-monotonous declarations appropriately. Minor INCOMPATIBILITY.

*** HOL ***

* The Nunchaku model finder is now part of "Main".

* SMT module:

  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to

    'int' and benefit from the SMT solver's theory reasoning. It is

    disabled by default.

  - The legacy module "src/HOL/Library/Old_SMT.thy" has been removed.

  - Several small issues have been rectified in the 'smt' command.

* (Co)datatype package: The 'size_gen_o_map' lemma is no longer

generated for datatypes with type class annotations. As a result, the

tactic that derives it no longer fails on nested datatypes. Slight

INCOMPATIBILITY.

* Command and antiquotation "value" with modified default strategy:

terms without free variables are always evaluated using plain evaluation

only, with no fallback on normalization by evaluation. Minor

INCOMPATIBILITY.

* Theories "GCD" and "Binomial" are already included in "Main" (instead

of "Complex_Main").

* Constant "surj" is a full input/output abbreviation (again).

Minor INCOMPATIBILITY.

* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.

INCOMPATIBILITY.

* Renamed ii to imaginary_unit in order to free up ii as a variable

name. The syntax \<i> remains available. INCOMPATIBILITY.

* Dropped abbreviations transP, antisymP, single_valuedP; use constants

transp, antisymp, single_valuedp instead. INCOMPATIBILITY.

* Constant "subseq" in Topological_Spaces has been removed -- it is

subsumed by "strict_mono". Some basic lemmas specific to "subseq" have

been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.

* Theory List: "sublist" renamed to "nths" in analogy with "nth", and

"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.

* Theory List: new generic function "sorted_wrt".

* Named theorems mod_simps covers various congruence rules concerning

mod, replacing former zmod_simps. INCOMPATIBILITY.

* Swapped orientation of congruence rules mod_add_left_eq,

mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,

mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,

mod_diff_eq. INCOMPATIBILITY.

* Generalized some facts:

    measure_induct_rule

    measure_induct

    zminus_zmod ~> mod_minus_eq

    zdiff_zmod_left ~> mod_diff_left_eq

    zdiff_zmod_right ~> mod_diff_right_eq

    zmod_eq_dvd_iff ~> mod_eq_dvd_iff

INCOMPATIBILITY.

* Algebraic type class hierarchy of euclidean (semi)rings in HOL:

euclidean_(semi)ring, euclidean_(semi)ring_cancel,

unique_euclidean_(semi)ring; instantiation requires provision of a

euclidean size.

* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked:

  - Euclidean induction is available as rule eucl_induct.

  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,

    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow

    easy instantiation of euclidean (semi)rings as GCD (semi)rings.

  - Coefficients obtained by extended euclidean algorithm are

    available as "bezout_coefficients".

INCOMPATIBILITY.

* Theory "Number_Theory.Totient" introduces basic notions about Euler's

totient function previously hidden as solitary example in theory

Residues. Definition changed so that "totient 1 = 1" in agreement with

the literature. Minor INCOMPATIBILITY.

* New styles in theory "HOL-Library.LaTeXsugar":

  - "dummy_pats" for printing equations with "_" on the lhs;

  - "eta_expand" for printing eta-expanded terms.

* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has

been renamed to bij_swap_compose_bij. INCOMPATIBILITY.

* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"

filter for describing points x such that f(x) is in the filter F.

* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been

renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name

space. INCOMPATIBILITY.

* Theory "HOL-Library.FinFun" has been moved to AFP (again).

INCOMPATIBILITY.

* Theory "HOL-Library.FuncSet": 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:

syntax (ASCII)

  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)

  "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)

  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)

* Theory "HOL-Library.Multiset": the simprocs on subsets operators of

multisets have been renamed:

  msetless_cancel_numerals ~> msetsubset_cancel

  msetle_cancel_numerals ~> msetsubset_eq_cancel

INCOMPATIBILITY.

* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax

for pattern aliases as known from Haskell, Scala and ML.

* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.

* Session HOL-Analysis: more material involving arcs, paths, covering

spaces, innessential maps, retracts, infinite products, simplicial

complexes. Baire Category theorem. Major results include the Jordan

Curve Theorem and the Great Picard Theorem.

* Session HOL-Algebra has been extended by additional lattice theory:

the Knaster-Tarski fixed point theorem and Galois Connections.

* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions

of squarefreeness, n-th powers, and prime powers.

* Session "HOL-Computional_Algebra" covers many previously scattered

theories, notably Euclidean_Algorithm, Factorial_Ring,

Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra,

Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor

INCOMPATIBILITY.

*** System ***

* Isabelle/Scala: the SQL module supports access to relational

databases, either as plain file (SQLite) or full-scale server

(PostgreSQL via local port or remote ssh connection).

* Results of "isabelle build" are recorded as SQLite database (i.e.

"Application File Format" in the sense of

https://www.sqlite.org/appfileformat.html). This allows systematic

access via operations from module Sessions.Store in Isabelle/Scala.

* System option "parallel_proofs" is 1 by default (instead of more

aggressive 2). This requires less heap space and avoids burning parallel

CPU cycles, while full subproof parallelization is enabled for repeated

builds (according to parallel_subproofs_threshold).

* System option "record_proofs" allows to change the global

Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;

a negative value means the current state in the ML heap image remains

unchanged.

* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been

renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY.

* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM,

ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the

native Windows platform (independently of the Cygwin installation). This

is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,

ISABELLE_PLATFORM64.

* Command-line tool "isabelle build_docker" builds a Docker image from

the Isabelle application bundle for Linux. See also

https://hub.docker.com/r/makarius/isabelle

* Command-line tool "isabelle vscode_server" provides a Language Server

Protocol implementation, e.g. for the Visual Studio Code editor. It

serves as example for alternative PIDE front-ends.

* Command-line tool "isabelle imports" helps to maintain theory imports

wrt. session structure. Examples for the main Isabelle distribution:

  isabelle imports -I -a

  isabelle imports -U -a

  isabelle imports -U -i -a

  isabelle imports -M -a -d '~~/src/Benchmarks'

New in Isabelle2016-1 (December 2016)

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

*** General ***

* Splitter in proof methods "simp", "auto" and friends:

  - The syntax "split add" has been discontinued, use plain "split",

    INCOMPATIBILITY.

  - For situations with many conditional or case expressions, there is

    an alternative splitting strategy that can be much faster. It is

    selected by writing "split!" instead of "split". It applies safe

    introduction and elimination rules after each split rule. As a

    result the subgoal may be split into several subgoals.

* Command 'bundle' provides a local theory target to define a bundle

from the body of specification commands (such as 'declare',

'declaration', 'notation', 'lemmas', 'lemma'). For example:

bundle foo

begin

  declare a [simp]

  declare b [intro]

end

* Command 'unbundle' is like 'include', but works within a local theory

context. Unlike "context includes ... begin", the effect of 'unbundle'

on the target context persists, until different declarations are given.

* Simplified outer syntax: uniform category "name" includes long

identifiers. Former "xname" / "nameref" / "name reference" has been

discontinued.

* Embedded content (e.g. the inner syntax of types, terms, props) may be

delimited uniformly via cartouches. This works better than old-fashioned

quotes when sub-languages are nested.

* Mixfix annotations support general block properties, with syntax

"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",

"unbreakable", "markup". The existing notation "(DIGITS" is equivalent

to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks

is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.

* Proof method "blast" is more robust wrt. corner cases of Pure

statements without object-logic judgment.

* Commands 'prf' and 'full_prf' are somewhat more informative (again):

proof terms are reconstructed and cleaned from administrative thm nodes.

* Code generator: config option "code_timing" triggers measurements of

different phases of code generation. See src/HOL/ex/Code_Timing.thy for

examples.

* Code generator: implicits in Scala (stemming from type class

instances) are generated into companion object of corresponding type

class, to resolve some situations where ambiguities may occur.

* Solve direct: option "solve_direct_strict_warnings" gives explicit

warnings for lemma statements with trivial proofs.

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

* More aggressive flushing of machine-generated input, according to

system option editor_generated_input_delay (in addition to existing

editor_input_delay for regular user edits). This may affect overall PIDE

reactivity and CPU usage.

* Syntactic indentation according to Isabelle outer syntax. Action

"indent-lines" (shortcut C+i) indents the current line according to

command keywords and some command substructure. Action

"isabelle.newline" (shortcut ENTER) indents the old and the new line

according to command keywords only; see also option

"jedit_indent_newline".

* Semantic indentation for unstructured proof scripts ('apply' etc.) via

number of subgoals. This requires information of ongoing document

processing and may thus lag behind, when the user is editing too

quickly; see also option "jedit_script_indent" and

"jedit_script_indent_limit".

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'

are treated as delimiters for fold structure; 'begin' and 'end'

structure of theory specifications is treated as well.

* Command 'proof' provides information about proof outline with cases,

e.g. for proof methods "cases", "induct", "goal_cases".

* Completion templates for commands involving "begin ... end" blocks,

e.g. 'context', 'notepad'.

* Sidekick parser "isabelle-context" shows nesting of context blocks

according to 'begin' and 'end' structure.

* Highlighting of entity def/ref positions wrt. cursor.

* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all

occurrences of the formal entity at the caret position. This facilitates

systematic renaming.

* PIDE document markup works across multiple Isar commands, e.g. the

results established at the end of a proof are properly identified in the

theorem statement.

* Cartouche abbreviations work both for " and ` to accomodate typical

situations where old ASCII notation may be updated.

* Dockable window "Symbols" also provides access to 'abbrevs' from the

outer syntax of the current theory buffer. This provides clickable

syntax templates, including entries with empty abbrevs name (which are

inaccessible via keyboard completion).

* IDE support for the Isabelle/Pure bootstrap process, with the

following independent stages:

  src/Pure/ROOT0.ML

  src/Pure/ROOT.ML

  src/Pure/Pure.thy

  src/Pure/ML_Bootstrap.thy

The ML ROOT files act like quasi-theories in the context of theory

ML_Bootstrap: this allows continuous checking of all loaded ML files.

The theory files are presented with a modified header to import Pure

from the running Isabelle instance. Results from changed versions of

each stage are *not* propagated to the next stage, and isolated from the

actual Isabelle/Pure that runs the IDE itself. The sequential

dependencies of the above files are only observed for batch build.

* Isabelle/ML and Standard ML files are presented in Sidekick with the

tree structure of section headings: this special comment format is

described in "implementation" chapter 0, e.g. (*** section ***).

* Additional abbreviations for syntactic completion may be specified

within the theory header as 'abbrevs'. The theory syntax for 'keywords'

has been simplified accordingly: optional abbrevs need to go into the

new 'abbrevs' section.

* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and

$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor

INCOMPATIBILITY, use 'abbrevs' within theory header instead.

* Action "isabelle.keymap-merge" asks the user to resolve pending

Isabelle keymap changes that are in conflict with the current jEdit

keymap; non-conflicting changes are always applied implicitly. This

action is automatically invoked on Isabelle/jEdit startup and thus

increases chances that users see new keyboard shortcuts when re-using

old keymaps.

* ML and document antiquotations for file-systems paths are more uniform

and diverse:

  @{path NAME}   -- no file-system check

  @{file NAME}   -- check for plain file

  @{dir NAME}    -- check for directory

Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may

have to be changed.

*** Document preparation ***

* New symbol \<circle>, e.g. for temporal operator.

* New document and ML antiquotation @{locale} for locales, similar to

existing antiquotation @{class}.

* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --

this allows special forms of document output.

* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control

symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its

derivatives.

* \<^raw:...> symbols are no longer supported.

* Old 'header' command is no longer supported (legacy since

Isabelle2015).

*** Isar ***

* Many specification elements support structured statements with 'if' /

'for' eigen-context, e.g. 'axiomatization', 'abbreviation',

'definition', 'inductive', 'function'.

* Toplevel theorem statements support eigen-context notation with 'if' /

'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the

traditional long statement form (in prefix). Local premises are called

"that" or "assms", respectively. Empty premises are *not* bound in the

context: INCOMPATIBILITY.

* Command 'define' introduces a local (non-polymorphic) definition, with

optional abstraction over local parameters. The syntax resembles

'definition' and 'obtain'. It fits better into the Isar language than

old 'def', which is now a legacy feature.

* Command 'obtain' supports structured statements with 'if' / 'for'

context.

* Command '\<proof>' is an alias for 'sorry', with different