NEWS

updated for release;

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

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


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

*** General ***

* Session ROOT files need to specify explicit 'directories' for import
of theory files. Directories cannot be shared by different sessions.
(Recall that import of theories from other sessions works via
session-qualified theory names, together with suitable 'sessions'
declarations in the ROOT.)

* Internal derivations record dependencies on oracles and other theorems
accurately, including the implicit type-class reasoning wrt. proven
class relations and type arities. In particular, the formal tagging with
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
propagated properly to theorems depending on such type instances.

* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
actual proposition that is assumed in the goal and proof context. This
requires at least Proofterm.proofs = 1 to show up in theorem
dependencies.

* Command 'thm_oracles' prints all oracles used in given theorems,
covering the full graph of transitive dependencies.

* Command 'thm_deps' prints immediate theorem dependencies of the given
facts. The former graph visualization has been discontinued, because it
was hardly usable.


*** Isar ***

* The proof method combinator (subproofs m) applies the method
expression m consecutively to each subgoal, constructing individual
subproofs internally. This impacts the internal construction of proof
terms: it makes a cascade of let-expressions within the derivation tree
and may thus improve scalability.

* Attribute "trace_locales" activates tracing of locale instances during
roundup. It replaces the diagnostic command 'print_dependencies', which
has been discontinued.


*** Isabelle/jEdit Prover IDE ***

* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
the "session focus" of option "isabelle jedit -S" has become obsolete
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
sufficient and more convenient to start editing a particular session.

* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).


*** HOL ***

* Improvements of the 'lift_bnf' command:
  - Add support for quotient types.
  - Generate transfer rules for the lifted map/set/rel/pred constants
    (theorems "<type>.<constant>_transfer_raw").

* Term_XML.Encode/Decode.term uses compact representation of Const
"typargs" from the given declaration environment. This also makes more
sense for translations to lambda-calculi with explicit polymorphism.
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special
applications.

* ASCII membership syntax concerning big operators for infimum and
supremum has been discontinued. INCOMPATIBILITY.

* Clear distinction between types for bits (False / True) and Z2 (0 /
1): theory HOL-Library.Bit has been renamed accordingly.
INCOMPATIBILITY.

* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond
to algebra_simps and field_simps but contain more aggressive rules
potentially splitting goals; algebra_split_simps roughly replaces
sign_simps and field_split_simps can be used instead of divide_simps.
INCOMPATIBILITY.

* Theory HOL.Complete_Lattices:
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf

* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>)
associates to the left now as is customary.

* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with
multiple colours and arbitrary exponents.

* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.

* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
INCOMPATIBILITY.

* Session HOL-Proofs: build faster thanks to better treatment of proof
terms in Isabelle/Pure.


*** ML ***

* Theory construction may be forked internally, the operation
Theory.join_theory recovers a single result theory. See also the example
in theory "HOL-ex.Join_Theory".

* Antiquotation @{oracle_name} inlines a formally checked oracle name.

* Minimal support for a soft-type system within the Isabelle logical
framework (module Soft_Type_System).

* Former Proof_Context.auto_fixes has been replaced by slightly more
general Proof_Context.augment: it is subject to an optional soft-type
system of the underlying object-logic. Minor INCOMPATIBILITY.

* More scalable Export.export using XML.tree to avoid premature string
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY.


*** System ***

* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot>

* The command-line tool "isabelle scala_project" creates a Gradle
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs
such as IntelliJ IDEA.

* The command-line tool "isabelle phabricator_setup" facilitates
self-hosting of the Phabricator software-development platform, with
support for Git, Mercurial, Subversion repositories. This helps to avoid
monoculture and to escape the gravity of centralized version control by
Github and/or Bitbucket. For further documentation, see chapter
"Phabricator server administration" in the "system" manual. A notable
example installation is https://isabelle-dev.sketis.net/.

* The command-line tool "isabelle hg_setup" simplifies the setup of
Mercurial repositories, with hosting via Phabricator or SSH file server
access.

* The command-line tool "isabelle imports" has been discontinued: strict
checking of session directories enforces session-qualified theory names
in applications -- users are responsible to specify session ROOT entries
properly.

* The command-line tool "isabelle dump" and its underlying
Isabelle/Scala module isabelle.Dump has become more scalable, by
splitting sessions and supporting a base logic image. Minor
INCOMPATIBILITY in options and parameters.

* Isabelle/Scala support for the Linux platform (Ubuntu): packages,
users, system services.

* Isabelle/Scala support for proof terms (with full type/term
information) in module isabelle.Term.

* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now
exported as well: this spans an overall dependency graph of internal
inferences; it might help to reconstruct the formal structure of theory
libraries. See also the module Export_Theory in Isabelle/Scala.

* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM
have been discontinued -- deprecated since Isabelle2018.

* More complete x86_64 platform support on macOS, notably Catalina where
old x86 has been discontinued.

* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4.

* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before).



New in Isabelle2019 (June 2019)
-------------------------------

*** General ***

* The font collection "Isabelle DejaVu" is systematically derived from
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
"IsabelleText" font (which is no longer provided separately). The line
metrics and overall rendering quality is closer to original DejaVu.
INCOMPATIBILITY with display configuration expecting the old
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.

* The Isabelle fonts render "\<inverse>" properly as superscript "-1".

* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).

* Old-style {* verbatim *} tokens are explicitly marked as legacy
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
via "isabelle update_cartouches -t" (available since Isabelle2015).

* Infix operators that begin or end with a "*" are now parenthesized
without additional spaces, e.g. "(*)" instead of "( * )". Minor
INCOMPATIBILITY.

* Mixfix annotations may use cartouches instead of old-style double
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u
mixfix_cartouches" allows to update existing theory sources
automatically.

* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
need to provide a closed expression -- without trailing semicolon. Minor
INCOMPATIBILITY.

* Commands 'generate_file', 'export_generated_files', and
'compile_generated_files' support a stateless (PIDE-conformant) model
for generated sources and compiled binaries of other languages. The
compilation process is managed in Isabelle/ML, and results exported to
the session database for further use (e.g. with "isabelle export" or
"isabelle build -e").


*** Isabelle/jEdit Prover IDE ***

* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. Line spacing no longer needs to be
adjusted: properties for the old IsabelleText font had "Global Options /
Text Area / Extra vertical line spacing (in pixels): -2", it now
defaults to 1, but 0 works as well.

* The jEdit File Browser is more prominent in the default GUI layout of
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
resources, notably via "favorites:" (or "Edit Favorites").

* Further markup and rendering for "plain text" (e.g. informal prose)
and "raw text" (e.g. verbatim sources). This improves the visual
appearance of formal comments inside the term language, or in general
for repeated alternation of formal and informal text.

* Action "isabelle-export-browser" points the File Browser to the theory
exports of the current buffer, based on the "isabelle-export:" virtual
file-system. The directory view needs to be reloaded manually to follow
ongoing document processing.

* Action "isabelle-session-browser" points the File Browser to session
information, based on the "isabelle-session:" virtual file-system. Its
entries are structured according to chapter / session names, the open
operation is redirected to the session ROOT file.

* Support for user-defined file-formats via class isabelle.File_Format
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
the shell function "isabelle_file_format" in etc/settings (e.g. of an
Isabelle component).

* System option "jedit_text_overview" allows to disable the text
overview column.

* Command-line options "-s" and "-u" of "isabelle jedit" override the
default for system option "system_heaps" that determines the heap
storage directory for "isabelle build". Option "-n" is now clearly
separated from option "-s".

* The Isabelle/jEdit desktop application uses the same options as
"isabelle jedit" for its internal "isabelle build" process: the implicit
option "-o system_heaps" (or "-s") has been discontinued. This reduces
the potential for surprise wrt. command-line tools.

* The official download of the Isabelle/jEdit application already
contains heap images for Isabelle/HOL within its main directory: thus
the first encounter becomes faster and more robust (e.g. when run from a
read-only directory).

* Isabelle DejaVu fonts are available with hinting by default, which is
relevant for low-resolution displays. This may be disabled via system
option "isabelle_fonts_hinted = false" in
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better
results.

* OpenJDK 11 has quite different font rendering, with better glyph
shapes and improved sub-pixel anti-aliasing. In some situations results
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD
display is recommended.

* OpenJDK 11 supports GTK version 2.2 and 3 (according to system
property jdk.gtk.version). The factory default is version 3, but
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make
this more conservative (as in Java 8). Depending on the GTK theme
configuration, "-Djdk.gtk.version=3" might work better or worse.


*** Document preparation ***

* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
are stripped from document output: the effect is to modify the semantic
presentation context or to emit markup to the PIDE document. Some
predefined markers are taken from the Dublin Core Metadata Initiative,
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
can be retrieved from the document database.

* Old-style command tags %name are re-interpreted as markers with
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
before. Potential INCOMPATIBILITY: multiple markers are composed in
canonical order, resulting in a reversed list of tags in the
presentation context.

* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
of semantics wrt. old-style %name.

* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
template.

* Document antiquotation option "cartouche" indicates if the output
should be delimited as cartouche; this takes precedence over the
analogous option "quotes".

* Many document antiquotations are internally categorized as "embedded"
and expect one cartouche argument, which is typically used with the
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
delimiters are stripped in output of the source (antiquotation option
"source"), but it is possible to enforce delimiters via option
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.


*** Isar ***

* Implicit cases goal1, goal2, goal3, etc. have been discontinued
(legacy feature since Isabelle2016).

* More robust treatment of structural errors: begin/end blocks take
precedence over goal/proof. This is particularly relevant for the
headless PIDE session and server.

* Command keywords of kind thy_decl / thy_goal may be more specifically
fit into the traditional document model of "definition-statement-proof"
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt.


*** HOL ***

* Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.

* Command 'export_code': the 'file' argument is now legacy and will be
removed soon: writing to the physical file-system is not well-defined in
a reactive/parallel application like Isabelle. The empty 'file' argument
has been discontinued already: it is superseded by the file-browser in
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.

* Command 'code_reflect' no longer supports the 'file' argument: it has
been superseded by 'file_prefix' for stateless file management as in
'export_code'. Minor INCOMPATIBILITY.

* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.

* Code generation for OCaml: Zarith supersedes Nums as library for
proper integer arithmetic. The library is located via standard
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
The environment provided by "isabelle ocaml_setup" already contains this
tool and the required packages. Minor INCOMPATIBILITY.

* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
INCOMPATIBILITY.

* Code generation: slightly more conventional syntax for 'code_stmts'
antiquotation. Minor INCOMPATIBILITY.

* Theory List: the precedence of the list_update operator has changed:
"f a [n := x]" now needs to be written "(f a)[n := x]".

* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators)
now have the same precedence as any other prefix function symbol. Minor
INCOMPATIBILITY.

* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
SUPREMUM, UNION, INTER should now rarely occur in output and are just
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
are gone INCOMPATIBILITY.

* The simplifier uses image_cong_simp as a congruence rule. The historic
and not really well-formed congruence rules INF_cong*, SUP_cong*, are
not used by default any longer. INCOMPATIBILITY; consider using declare
image_cong_simp [cong del] in extreme situations.

* INF_image and SUP_image are no default simp rules any longer.
INCOMPATIBILITY, prefer image_comp as simp rule if needed.

* Strong congruence rules (with =simp=> in the premises) for constant f
are now uniformly called f_cong_simp, in accordance with congruence
rules produced for mappers by the datatype package. INCOMPATIBILITY.

* Retired lemma card_Union_image; use the simpler card_UN_disjoint
instead. INCOMPATIBILITY.

* Facts sum_mset.commute and prod_mset.commute have been renamed to
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.

* ML structure Inductive: slightly more conventional naming schema.
Minor INCOMPATIBILITY.

* ML: Various _global variants of specification tools have been removed.
Minor INCOMPATIBILITY, prefer combinators
Named_Target.theory_map[_result] to lift specifications to the global
theory level.

* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports
overlapping and non-exhaustive patterns and handles arbitrarily nested
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which
assumes sequential left-to-right pattern matching. The generated
equation no longer tuples the arguments on the right-hand side.
INCOMPATIBILITY.

* Theory HOL-Library.Multiset: the \<Union># operator now has the same
precedence as any other prefix function symbol.

* Theory HOL-Library.Cardinal_Notations has been discontinued in favor
of the bundle cardinal_syntax (available in theory Main). Minor
INCOMPATIBILITY.

* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
used for computing powers in class "monoid_mult" and modular
exponentiation.

* Session HOL-Computational_Algebra: Formal Laurent series and overhaul
of Formal power series.

* Session HOL-Number_Theory: More material on residue rings in
Carmichael's function, primitive roots, more properties for "ord".

* Session HOL-Analysis: Better organization and much more material
at the level of abstract topological spaces.

* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
 algebraic closure of a field by de Vilhena and Baillon.

* Session HOL-Homology has been added. It is a port of HOL Light's
homology library, with new proofs of "invariance of domain" and related
results.

* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved via "isabelle build -e HOL-SPARK-Examples" on the
command-line.

* Sledgehammer:
  - The URL for SystemOnTPTP, which is used by remote provers, has been
    updated.
  - The machine-learning-based filter MaSh has been optimized to take
    less time (in most cases).

* SMT: reconstruction is now possible using the SMT solver veriT.

* Session HOL-Word:
  * New theory More_Word as comprehensive entrance point.
  * Merged type class bitss into type class bits.
  INCOMPATIBILITY.


*** ML ***

* Command 'generate_file' allows to produce sources for other languages,
with antiquotations in the Isabelle context (only the control-cartouche
form). The default "cartouche" antiquotation evaluates an ML expression
of type string and inlines the result as a string literal of the target
language. For example, this works for Haskell as follows:

  generate_file "Pure.hs" = \<open>
  module Isabelle.Pure where
    allConst, impConst, eqConst :: String
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
  \<close>

See also commands 'export_generated_files' and 'compile_generated_files'
to use the results.

* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
option ML_environment to select a named environment, such as "Isabelle"
for Isabelle/ML, or "SML" for official Standard ML.

* ML antiquotation @{master_dir} refers to the master directory of the
underlying theory, i.e. the directory of the theory file.

* ML antiquotation @{verbatim} inlines its argument as string literal,
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly
useful.

* Local_Theory.reset is no longer available in user space. Regular
definitional packages should use balanced blocks of
Local_Theory.open_target versus Local_Theory.close_target instead, or
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.

* Original PolyML.pointerEq is retained as a convenience for tools that
don't use Isabelle/ML (where this is called "pointer_eq").


*** System ***

* Update to OpenJDK 11: the current long-term support version of Java.

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.

* System option "checkpoint" has been discontinued: obsolete thanks to
improved memory management in Poly/ML.

* System option "system_heaps" determines where to store the session
image of "isabelle build" (and other tools using that internally).
Former option "-s" is superseded by option "-o system_heaps".
INCOMPATIBILITY in command-line syntax.

* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.

* The command-line tool "isabelle build -e" retrieves theory exports
from the session build database, using 'export_files' in session ROOT
entries.

* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
section "Theory update". Theory sessions are specified as in "isabelle
dump".

* The command-line tool "isabelle update -u control_cartouches" changes
antiquotations into control-symbol format (where possible): @{NAME}
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.

* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).

* Isabelle Server command "use_theories" supports "nodes_status_delay"
for continuous output of node status information. The time interval is
specified in seconds; a negative value means it is disabled (default).

* Isabelle Server command "use_theories" terminates more robustly in the
presence of structurally broken sources: full consolidation of theories
is no longer required.

* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
which needs to point to a suitable version of "ocamlfind" (e.g. via
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
ISABELLE_OCAMLC are no longer supported.

* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:

  isabelle ghc_setup
  isabelle ghc_stack

  isabelle ocaml_setup
  isabelle ocaml_opam

The global installation state is determined by the following settings
(and corresponding directory contents):

  ISABELLE_STACK_ROOT
  ISABELLE_STACK_RESOLVER
  ISABELLE_GHC_VERSION

  ISABELLE_OPAM_ROOT
  ISABELLE_OCAML_VERSION

After setup, the following Isabelle settings are automatically
redirected (overriding existing user settings):

  ISABELLE_GHC

  ISABELLE_OCAMLFIND

The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
ISABELLE_OPAM_ROOT, or by resetting these variables in
$ISABELLE_HOME_USER/etc/settings.



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

* Global facts need to be closed: no free variables and no hypotheses.
Rare INCOMPATIBILITY.

* Facts stemming from locale interpretation are subject to lazy
evaluation for improved performance. Rare INCOMPATIBILITY: errors
stemming from interpretation morphisms might be deferred and thus
difficult to locate; enable system option "strict_facts" temporarily to
avoid this.

* 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, use the command-line tool "isabelle update_op" to
convert 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

  - option -i includes additional sessions into the name-space of
    theories

  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
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL

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

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

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

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

* Command-line tool "isabelle vscode_server" accepts the same options
-A, -R, -S, -i for session selection as "isabelle jedit". This is
relevant for isabelle.args configuration settings in VSCode. The former
option -A (explore all known session files) has been discontinued: it is
enabled by default, unless option -S is used to focus on a particular
spot in the session structure. INCOMPATIBILITY.


*** 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 alternative command tags. 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 @{theory name} requires the long
session-qualified theory name: this is what users reading the text
normally need to import.

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


*** Pure ***

* The inner syntax category "sort" now includes notation "_" for the
dummy sort: it is effectively ignored in type-inference.

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


*** HOL ***

* Sledgehammer: bundled version of "vampire" (for non-commercial users)
helps to avoid fragility of "remote_vampire" service.

* 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 the theories
HOL-ex.Code_Lazy_Demo and 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: the Arg function now respects the same interval
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.

* Session HOL-Analysis: the functions zorder, zer_poly, porder and
pol_poly have been redefined. All related lemmas have been reworked.
INCOMPATIBILITY.

* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.

* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
or real-valued functions (limits, "Big-O", etc.) automatically.
See also ~~/src/HOL/Real_Asymp/Manual for some documentation.

* Session HOL-Types_To_Sets: more tool support (unoverload_type combines
internalize_sorts and unoverload) and larger experimental application
(type based linear algebra transferred to linear algebra on subspaces).


*** 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" options -c -x -B refer to
descendants wrt. the session parent or import graph. Subtle
INCOMPATIBILITY: options -c -x used to refer to the session parent graph
only.

* 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_HEAPS + ISABELLE_BROWSER_INFO (or
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
mode") determine the directory locations of the main build artefacts --
instead of hard-wired directories in ISABELLE_HOME_USER (or
ISABELLE_HOME).

* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
heap images and session databases are always stored in
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
$ISABELLE_HEAPS_SYSTEM/$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.