diff --git a/CONTRIBUTORS b/CONTRIBUTORS
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -1,1100 +1,1104 @@
For the purposes of the license agreement in the file COPYRIGHT, a
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2022
-----------------------------
* August 2022: Norbert Schirmer, Apple
Record simproc that sorts update expressions.
* June 2022: Jan van Brügge, TU München
Strict cardinality bounds for BNFs.
* April - August 2021: Denis Paluca and Fabian Huch, TU München
Various improvements to Isabelle/VSCode.
* March 2021: Florian Haftmann, TU München
More ambitious minimization of case expressions in generated code;
code generation: type annotations in pattern bindings are printed in a
way suitable for Scala 3.
* July 2022: Florian Haftmann, TU München and René Thiemann, UIBK
Theory Code_Abstract_Char implements characters by target language
integers, sacrificing pattern patching in exchange for dramatically
increased performance for comparisions.
* November 2021, July - August 2022: Fabian Huch and Makarius Wenzel
Improved HTML presentation.
Contributions to Isabelle2021-1
-------------------------------
* September / October 2021: Jasmin Blanchette, Martin Desharnais,
Mathias Fleury, Makarius Wenzel
Upgrade of automatic theorem provers in Sledgehammer and the "smt" proof
method.
* July - September 2021: Makarius Wenzel
Significantly improved Isabelle/Haskell library.
* July - September 2021: Jasmin Blanchette, Martin Desharnais
Various improvements to Sledgehammer.
* September 2021: Dominique Unruh
New theory of infinite sums (theory HOL-Analysis.Infinite_Sum), ordering of
complex numbers (theory HOL-Library.Complex_Order), and products of uniform
spaces (theory HOL-Analysis.Product_Vector).
* August 2021: Fabian Huch, TU München
Improved HTML presentation: links to formal entities.
* November 2020 / July 2021: Norbert Schirmer, Apple
Various improvements and cleanup of session "HOL-Statespace".
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
* June 2021: Florian Haftmann
More context situations susceptible to global_interpretation.
* March 2021: Lukas Stevens
New order prover.
* March 2021: Florian Haftmann
Dedicated session for combinatorics.
* March 2021: Simon Foster and Leo Freitas
More symbol definitions for Z Notation: Isabelle fonts and LaTeX macros.
* February 2021: Manuel Eberl
New material in sessions HOL-Analysis and HOL-Probability, most notably
Hoeffding's inequality and the negative binomial distribution
* January 2021: Jakub Kądziołka
Some lemmas for HOL-Computational_Algebra.
* January 2021: Martin Rasyzk
Fast set operations for red-black trees.
Contributions to Isabelle2021
-----------------------------
* January 2021: Manuel Eberl
Characteristic of a semiring.
* January 2021: Manuel Eberl
Algebraic integers in HOL-Computational_Algebra.
* December 2020: Stepan Holub
Contributed lemmas for theory HOL.List.
* December 2020: Martin Desharnais
Zipperposition 2.0 as external prover for Sledgehammer.
* December 2020: Walter Guttmann
Extension of session HOL-Hoare with total correctness proof system.
* November / December 2020: Makarius Wenzel
Improved HTML presentation and PDF document preparation, using mostly
Isabelle/Scala instead of Isabelle/ML.
* November 2020: Stepan Holub
Removed preconditions from lemma comm_append_are_replicate.
* November 2020: Florian Haftmann
Bundle mixins for locale and class expressions.
* November 2020: Jakub Kądziołka
Stronger lemmas about orders of group elements (generate_pow_card).
* October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury
Support veriT as external prover in Sledgehammer.
* October 2020: Mathias Fleury
Updated proof reconstruction for the SMT solver veriT in the smt method.
* October 2020: Jasmin Blanchette, Martin Desharnais
Support E prover 2.5 as external prover in Sledgehammer.
* September 2020: Florian Haftmann
Substantial reworking and modularization of Word library, with generic type
conversions.
* August 2020: Makarius Wenzel
Finally enable PIDE protocol for batch-builds, with various consequences of
handling session build databases, Isabelle/Scala within Isabelle/ML etc.
* August 2020: Makarius Wenzel
Improved monitoring of runtime statistics: ML GC progress and Java.
* July 2020: Martin Desharnais
Update to Metis 2.4.
* June 2020: Makarius Wenzel
Batch-builds via "isabelle build" allow to invoke Scala from ML.
* June 2020: Florian Haftmann
Simproc defined_all for more aggressive substitution with variables
from assumptions.
* May 2020: Makarius Wenzel
Antiquotations for Isabelle systems programming, notably @{scala_function}
and @{scala} to invoke Scala from ML.
* May 2020: Florian Haftmann
Generic algebraically founded bit operations NOT, AND, OR, XOR.
Contributions to Isabelle2020
-----------------------------
* February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
Simplified, generalised version of ZF/Constructible.
* January 2020: LC Paulson
The full finite Ramsey's theorem and elements of finite and infinite
Ramsey theory.
* December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy
Traytel
Extension of lift_bnf to support quotient types.
* November 2019: Peter Zeller, TU Kaiserslautern
Update of Isabelle/VSCode to WebviewPanel API.
* October..December 2019: Makarius Wenzel
Isabelle/Phabrictor server setup, including Linux platform support in
Isabelle/Scala. Client-side tool "isabelle hg_setup".
* October 2019: Maximilian Schäffeler
Port of the HOL Light decision procedure for metric spaces.
* October 2019: Makarius Wenzel
More scalable Isabelle dump and underlying headless PIDE session.
* August 2019: Makarius Wenzel
Better support for proof terms in Isabelle/Pure, notably via method
combinator SUBPROOFS (ML) and "subproofs" (Isar).
* July 2019: Alexander Krauss, Makarius Wenzel
Minimal support for a soft-type system within the Isabelle logical
framework.
Contributions to Isabelle2019
-----------------------------
* April 2019: LC Paulson
Homology and supporting lemmas on topology and group theory
* April 2019: Paulo de Vilhena and Martin Baillon
Group theory developments, esp. algebraic closure of a field
* February/March 2019: Makarius Wenzel
Stateless management of export artifacts in the Isabelle/HOL code generator.
* February 2019: Manuel Eberl
Exponentiation by squaring, used to implement "power" in monoid_mult and
fast modular exponentiation.
* February 2019: Manuel Eberl
Carmichael's function, primitive roots in residue rings, more properties of
the order in residue rings.
* February 2019: Jeremy Sylvestre
Formal Laurent Series and overhaul of Formal power series.
* January 2019: Florian Haftmann
Clarified syntax and congruence rules for big operators on sets involving
the image operator.
* January 2019: Florian Haftmann
Renovation of code generation, particularly export into session data and
proper strings and proper integers based on zarith for OCaml.
* January 2019: Andreas Lochbihler
New implementation for case_of_simps based on Code_Lazy's pattern matching
elimination algorithm.
* November/December 2018: Makarius Wenzel
Support for Isabelle/Haskell applications of Isabelle/PIDE.
* August/September 2018: Makarius Wenzel
Improvements of headless Isabelle/PIDE session and server, and systematic
exports from theory documents.
* December 2018: Florian Haftmann
Generic executable sorting algorithms based on executable comparators.
* October 2018: Mathias Fleury
Proof reconstruction for the SMT solver veriT in the smt method.
Contributions to Isabelle2018
-----------------------------
* July 2018: Manuel Eberl
"real_asymp" proof method for automatic proofs of real limits, "Big-O"
statements, etc.
* June 2018: Fabian Immler
More tool support for HOL-Types_To_Sets.
* June 2018: Martin Baillon and Paulo Emílio de Vilhena
A variety of contributions to HOL-Algebra.
* June 2018: Wenda Li
New/strengthened results involving analysis, topology, etc.
* May/June 2018: Makarius Wenzel
System infrastructure to export blobs as theory presentation, and to dump
PIDE database content in batch mode.
* May 2018: Manuel Eberl
Landau symbols and asymptotic equivalence (moved from the AFP).
* May 2018: Jose Divasón (Universidad de la Rioja),
Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
Fabian Immler (TUM)
Generalizations in the formalization of linear algebra.
* May 2018: Florian Haftmann
Consolidation of string-like types in HOL.
* May 2018: Andreas Lochbihler (Digital Asset),
Pascal Stoop (ETH Zurich)
Code generation with lazy evaluation semantics.
* March 2018: Florian Haftmann
Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
algebraic foundation for bit strings and word types in HOL-ex.
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
* February 2018: Wenda Li
A unified definition for the order of zeros and poles. Improved reasoning
around non-essential singularities.
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
* December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
A new conditional parametricity prover.
* October 2017: Alexander Maletzky
Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
Contributions to Isabelle2017
-----------------------------
* September 2017: Lawrence Paulson
HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem.
* September 2017: Jasmin Blanchette
Further integration of Nunchaku model finder.
* November 2016 - June 2017: Makarius Wenzel
New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE.
* 2017: Makarius Wenzel
Session-qualified theory names (theory imports and ROOT files).
Prover IDE improvements.
Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
* August 2017: Andreas Lochbihler, ETH Zurich
type of unordered pairs (HOL-Library.Uprod)
* August 2017: Manuel Eberl, TUM
HOL-Analysis: infinite products over natural numbers,
infinite sums over arbitrary sets, connection between formal
power series and analytic complex functions
* March 2017: Alasdair Armstrong, University of Sheffield and
Simon Foster, University of York
Fixed-point theory and Galois Connections in HOL-Algebra.
* February 2017: Florian Haftmann, TUM
Statically embedded computations implemented by generated code.
Contributions to Isabelle2016-1
-------------------------------
* December 2016: Ondřej Kunčar, TUM
Types_To_Sets: experimental extension of Higher-Order Logic to allow
translation of types to sets.
* October 2016: Jasmin Blanchette
Integration of Nunchaku model finder.
* October 2016: Jaime Mendizabal Roche, TUM
Ported remaining theories of session Old_Number_Theory to the new
Number_Theory and removed Old_Number_Theory.
* September 2016: Sascha Boehme
Proof method "argo" based on SMT technology for a combination of
quantifier-free propositional logic, equality and linear real arithmetic
* July 2016: Daniel Stuewe
Height-size proofs in HOL-Data_Structures.
* July 2016: Manuel Eberl, TUM
Algebraic foundation for primes; generalization from nat to general
factorial rings.
* June 2016: Andreas Lochbihler, ETH Zurich
Formalisation of discrete subprobability distributions.
* June 2016: Florian Haftmann, TUM
Improvements to code generation: optional timing measurements, more succint
closures for static evaluation, less ambiguities concering Scala implicits.
* May 2016: Manuel Eberl, TUM
Code generation for Probability Mass Functions.
* March 2016: Florian Haftmann, TUM
Abstract factorial rings with unique factorization.
* March 2016: Florian Haftmann, TUM
Reworking of the HOL char type as special case of a finite numeral type.
* March 2016: Andreas Lochbihler, ETH Zurich
Reasoning support for monotonicity, continuity and admissibility in
chain-complete partial orders.
* February - October 2016: Makarius Wenzel
Prover IDE improvements.
ML IDE improvements: bootstrap of Pure.
Isar language consolidation.
Notational modernization of HOL.
Tight Poly/ML integration.
More Isabelle/Scala system programming modules (e.g. SSH, Mercurial).
* Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu,
Middlesex University, and Dmitriy Traytel, ETH Zurich
'corec' command and friends.
* January 2016: Florian Haftmann, TUM
Abolition of compound operators INFIMUM and SUPREMUM for complete lattices.
Contributions to Isabelle2016
-----------------------------
* Winter 2016: Manuel Eberl, TUM
Support for real exponentiation ("powr") in the "approximation" method.
(This was removed in Isabelle 2015 due to a changed definition of "powr".)
* Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
General, homology form of Cauchy's integral theorem and supporting material
(ported from HOL Light).
* Winter 2015/16: Gerwin Klein, NICTA
New print_record command.
* May - December 2015: Makarius Wenzel
Prover IDE improvements.
More Isar language elements.
Document language refinements.
Poly/ML debugger integration.
Improved multi-platform and multi-architecture support.
* Winter 2015: Manuel Eberl, TUM
The radius of convergence of power series and various summability tests.
Harmonic numbers and the Euler-Mascheroni constant.
The Generalised Binomial Theorem.
The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
most important properties.
* Autumn 2015: Manuel Eberl, TUM
Proper definition of division (with remainder) for formal power series;
Euclidean Ring and GCD instance for formal power series.
* Autumn 2015: Florian Haftmann, TUM
Rewrite definitions for global interpretations and sublocale declarations.
* Autumn 2015: Andreas Lochbihler
Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
partial orders.
* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
A large number of additional binomial identities.
* Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
Isar subgoal command for proof structure within unstructured proof scripts.
* Summer 2015: Florian Haftmann, TUM
Generic partial division in rings as inverse operation of multiplication.
* Summer 2015: Manuel Eberl and Florian Haftmann, TUM
Type class hierarchy with common algebraic notions of integral (semi)domains
like units, associated elements and normalization wrt. units.
* Summer 2015: Florian Haftmann, TUM
Fundamentals of abstract type class for factorial rings.
* Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
Command to lift a BNF structure on the raw type to the abstract type for
typedefs.
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
Proof of the central limit theorem: includes weak convergence,
characteristic functions, and Levy's uniqueness and continuity theorem.
Contributions to Isabelle2015
-----------------------------
* 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel
The Eisbach proof method language and "match" method.
* Winter 2014 and Spring 2015: Ondrej Kuncar, TUM
Extension of lift_definition to execute lifted functions that have as a
return type a datatype containing a subtype.
* March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
and Dmitriy Traytel, TUM
More multiset theorems, syntax, and operations.
* December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and
Jeremy Avigad, Luke Serafin, CMU
Various integration theorems: mostly integration on intervals and
substitution.
* September 2014: Florian Haftmann, TUM
Lexicographic order on functions and
sum/product over function bodies.
* August 2014: Andreas Lochbihler, ETH Zurich
Test infrastructure for executing generated code in target languages.
* August 2014: Manuel Eberl, TUM
Generic euclidean algorithms for GCD et al.
Contributions to Isabelle2014
-----------------------------
* July 2014: Thomas Sewell, NICTA
Preserve equality hypotheses in "clarify" and friends. New
"hypsubst_thin" method configuration option.
* Summer 2014: Florian Haftmann, TUM
Consolidation and generalization of facts concerning (abelian)
semigroups and monoids, particularly products (resp. sums) on
finite sets.
* Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
veriT, Waldmeister, etc.).
* June 2014: Florian Haftmann, TUM
Internal reorganisation of the local theory / named target stack.
* June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
Various properties of exponentially, Erlang, and normal distributed
random variables.
* May 2014: Cezary Kaliszyk, University of Innsbruck, and
Jasmin Blanchette, TUM
SML-based engines for MaSh.
* March 2014: René Thiemann
Improved code generation for multisets.
* February 2014: Florian Haftmann, TUM
Permanent interpretation inside theory, locale and class targets
with mixin definitions.
* Spring 2014: Lawrence C Paulson, Cambridge
Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
* Winter 2013 and Spring 2014: Ondrej Kuncar, TUM
Various improvements to Lifting/Transfer, integration with the BNF package.
* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny,
Dmitriy Traytel, and Jasmin Blanchette, TUM
Various improvements to the BNF-based (co)datatype package,
including a more polished "primcorec" command, optimizations, and
integration in the "HOL" session.
* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and
Jasmin Blanchette, TUM
"SMT2" module and "smt2" proof method, based on SMT-LIB 2 and
Z3 4.3.
* January 2014: Lars Hupel, TUM
An improved, interactive simplifier trace with integration into the
Isabelle/jEdit Prover IDE.
* December 2013: Florian Haftmann, TUM
Consolidation of abstract interpretations concerning min and max.
* November 2013: Florian Haftmann, TUM
Abolition of negative numeral literals in the logic.
Contributions to Isabelle2013-1
-------------------------------
* September 2013: Lars Noschinski, TUM
Conversion between function definitions as list of equations and
case expressions in HOL.
New library Simps_Case_Conv with commands case_of_simps,
simps_of_case.
* September 2013: Nik Sultana, University of Cambridge
Improvements to HOL/TPTP parser and import facilities.
* September 2013: Johannes Hölzl and Dmitriy Traytel, TUM
New "coinduction" method (residing in HOL-BNF) to avoid boilerplate.
* Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
* Summer 2013: Manuel Eberl, TUM
Generation of elimination rules in the function package.
New command "fun_cases".
* Summer 2013: Christian Sternagel, JAIST
Improved support for ad hoc overloading of constants, including
documentation and examples.
* Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
Jasmin Blanchette, TUM
Various improvements to the BNF-based (co)datatype package, including
"primrec_new" and "primcorec" commands and a compatibility layer.
* Spring and Summer 2013: Ondrej Kuncar, TUM
Various improvements of Lifting and Transfer packages.
* Spring 2013: Brian Huffman, Galois Inc.
Improvements of the Transfer package.
* Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
Jasmin Blanchette, TUM
Various improvements to MaSh, including a server mode.
* First half of 2013: Steffen Smolka, TUM
Further improvements to Sledgehammer's Isar proof generator.
* May 2013: Florian Haftmann, TUM
Ephemeral interpretation in local theories.
* May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
Spec_Check: A Quickcheck tool for Isabelle/ML.
* April 2013: Stefan Berghofer, secunet Security Networks AG
Dmitriy Traytel, TUM
Makarius Wenzel, Université Paris-Sud / LRI
Case translations as a separate check phase independent of the
datatype package.
* March 2013: Florian Haftmann, TUM
Reform of "big operators" on sets.
* March 2013: Florian Haftmann, TUM
Algebraic locale hierarchy for orderings and (semi)lattices.
* February 2013: Florian Haftmann, TUM
Reworking and consolidation of code generation for target language
numerals.
* February 2013: Florian Haftmann, TUM
Sieve of Eratosthenes.
Contributions to Isabelle2013
-----------------------------
* 2012: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
* Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen
Jasmin Blanchette, TUM
Implemented Machine Learning for Sledgehammer (MaSh).
* Fall 2012: Steffen Smolka, TUM
Various improvements to Sledgehammer's Isar proof generator,
including a smart type annotation algorithm and proof shrinking.
* December 2012: Alessandro Coglio, Kestrel
Contributions to HOL's Lattice library.
* November 2012: Fabian Immler, TUM
"Symbols" dockable for Isabelle/jEdit.
* November 2012: Fabian Immler, TUM
Proof of the Daniell-Kolmogorov theorem: the existence of the limit
of projective families.
* October 2012: Andreas Lochbihler, KIT
Efficient construction of red-black trees from sorted associative
lists.
* September 2012: Florian Haftmann, TUM
Lattice instances for type option.
* September 2012: Christian Sternagel, JAIST
Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
* August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
New BNF-based (co)datatype package.
* August 2012: Andrei Popescu and Dmitriy Traytel, TUM
Theories of ordinals and cardinals.
* July 2012: Makarius Wenzel, Université Paris-Sud / LRI
Advanced support for Isabelle sessions and build management, notably
"isabelle build".
* June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
Simproc for rewriting set comprehensions into pointfree expressions.
* May 2012: Andreas Lochbihler, KIT
Theory of almost everywhere constant functions.
* 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM
Graphview in Scala/Swing.
Contributions to Isabelle2012
-----------------------------
* April 2012: Johannes Hölzl, TUM
Probability: Introduced type to represent measures instead of
locales.
* April 2012: Johannes Hölzl, Fabian Immler, TUM
Float: Moved to Dyadic rationals to represent floating point numers.
* April 2012: Thomas Sewell, NICTA and
2010: Sascha Boehme, TUM
Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
equalities/inequalities.
* March 2012: Christian Sternagel, JAIST
Consolidated theory of relation composition.
* March 2012: Nik Sultana, University of Cambridge
HOL/TPTP parser and import facilities.
* March 2012: Cezary Kaliszyk, University of Innsbruck and
Alexander Krauss, QAware GmbH
Faster and more scalable Import mechanism for HOL Light proofs.
* January 2012: Florian Haftmann, TUM, et al.
(Re-)Introduction of the "set" type constructor.
* 2012: Ondrej Kuncar, TUM
New package Lifting, various improvements and refinements to the
Quotient package.
* 2011/2012: Jasmin Blanchette, TUM
Various improvements to Sledgehammer, notably: tighter integration
with SPASS, support for more provers (Alt-Ergo, iProver,
iProver-Eq).
* 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
Various refinements of local theory infrastructure.
Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
Contributions to Isabelle2011-1
-------------------------------
* September 2011: Peter Gammie
Theory HOL/Library/Saturated: numbers with saturated arithmetic.
* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
Refined theory on complete lattices.
* August 2011: Brian Huffman, Portland State University
Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
* June 2011: Brian Huffman, Portland State University
Proof method "countable_datatype" for theory Library/Countable.
* 2011: Jasmin Blanchette, TUM
Various improvements to Sledgehammer, notably: use of sound
translations, support for more provers (Waldmeister, LEO-II,
Satallax). Further development of Nitpick and 'try' command.
* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
Theory HOL/Library/Cset_Monad allows do notation for computable sets
(cset) via the generic monad ad-hoc overloading facility.
* 2011: Johannes Hölzl, Armin Heller, TUM and
Bogdan Grechuk, University of Edinburgh
Theory HOL/Library/Extended_Reals: real numbers extended with plus
and minus infinity.
* 2011: Makarius Wenzel, Université Paris-Sud / LRI
Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
Prover IDE.
Contributions to Isabelle2011
-----------------------------
* January 2011: Stefan Berghofer, secunet Security Networks AG
HOL-SPARK: an interactive prover back-end for SPARK.
* October 2010: Bogdan Grechuk, University of Edinburgh
Extended convex analysis in Multivariate Analysis.
* October 2010: Dmitriy Traytel, TUM
Coercive subtyping via subtype constraints.
* October 2010: Alexander Krauss, TUM
Command partial_function for function definitions based on complete
partial orders in HOL.
* September 2010: Florian Haftmann, TUM
Refined concepts for evaluation, i.e., normalization of terms using
different techniques.
* September 2010: Florian Haftmann, TUM
Code generation for Scala.
* August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
Improved Probability theory in HOL.
* July 2010: Florian Haftmann, TUM
Reworking and extension of the Imperative HOL framework.
* July 2010: Alexander Krauss, TUM and Christian Sternagel, University
of Innsbruck
Ad-hoc overloading. Generic do notation for monads.
Contributions to Isabelle2009-2
-------------------------------
* 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
Makarius Wenzel, TUM / LRI
Elimination of type classes from proof terms.
* April 2010: Florian Haftmann, TUM
Reorganization of abstract algebra type classes.
* April 2010: Florian Haftmann, TUM
Code generation for data representations involving invariants;
various collections avaiable in theories Fset, Dlist, RBT,
Mapping and AssocList.
* March 2010: Sascha Boehme, TUM
Efficient SHA1 library for Poly/ML.
* February 2010: Cezary Kaliszyk and Christian Urban, TUM
Quotient type package for Isabelle/HOL.
Contributions to Isabelle2009-1
-------------------------------
* November 2009, Brian Huffman, PSU
New definitional domain package for HOLCF.
* November 2009: Robert Himmelmann, TUM
Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
* November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
A tabled implementation of the reflexive transitive closure.
* November 2009: Lukas Bulwahn, TUM
Predicate Compiler: a compiler for inductive predicates to
equational specifications.
* November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
HOL-Boogie: an interactive prover back-end for Boogie and VCC.
* October 2009: Jasmin Blanchette, TUM
Nitpick: yet another counterexample generator for Isabelle/HOL.
* October 2009: Sascha Boehme, TUM
Extension of SMT method: proof-reconstruction for the SMT solver Z3.
* October 2009: Florian Haftmann, TUM
Refinement of parts of the HOL datatype package.
* October 2009: Florian Haftmann, TUM
Generic term styles for term antiquotations.
* September 2009: Thomas Sewell, NICTA
More efficient HOL/record implementation.
* September 2009: Sascha Boehme, TUM
SMT method using external SMT solvers.
* September 2009: Florian Haftmann, TUM
Refinement of sets and lattices.
* July 2009: Jeremy Avigad and Amine Chaieb
New number theory.
* July 2009: Philipp Meyer, TUM
HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
prover.
* July 2009: Florian Haftmann, TUM
New quickcheck implementation using new code generator.
* July 2009: Florian Haftmann, TUM
HOL/Library/Fset: an explicit type of sets; finite sets ready to use
for code generation.
* June 2009: Florian Haftmann, TUM
HOL/Library/Tree: search trees implementing mappings, ready to use
for code generation.
* March 2009: Philipp Meyer, TUM
Minimization tool for results from Sledgehammer.
Contributions to Isabelle2009
-----------------------------
* March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
Cambridge
Elementary topology in Euclidean space.
* March 2009: Johannes Hoelzl, TUM
Method "approximation", which proves real valued inequalities by
computation.
* February 2009: Filip Maric, Univ. of Belgrade
A Serbian theory.
* February 2009: Jasmin Christian Blanchette, TUM
Misc cleanup of HOL/refute.
* February 2009: Timothy Bourke, NICTA
New find_consts command.
* February 2009: Timothy Bourke, NICTA
"solves" criterion for find_theorems and auto_solve option
* December 2008: Clemens Ballarin, TUM
New locale implementation.
* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
Method "sizechange" for advanced termination proofs.
* November 2008: Timothy Bourke, NICTA
Performance improvement (factor 50) for find_theorems.
* 2008: Florian Haftmann, TUM
Various extensions and restructurings in HOL, improvements
in evaluation mechanisms, new module binding.ML for name bindings.
* October 2008: Fabian Immler, TUM
ATP manager for Sledgehammer, based on ML threads instead of Posix
processes. Additional ATP wrappers, including remote SystemOnTPTP
services.
* September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
Prover for coherent logic.
* August 2008: Fabian Immler, TUM
Vampire wrapper script for remote SystemOnTPTP service.
Contributions to Isabelle2008
-----------------------------
* 2007/2008:
Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
HOL library improvements.
* 2007/2008: Brian Huffman, PSU
HOLCF library improvements.
* 2007/2008: Stefan Berghofer, TUM
HOL-Nominal package improvements.
* March 2008: Markus Reiter, TUM
HOL/Library/RBT: red-black trees.
* February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
Lukas Bulwahn, TUM and John Matthews, Galois:
HOL/Library/Imperative_HOL: Haskell-style imperative data structures
for HOL.
* December 2007: Norbert Schirmer, Uni Saarbruecken
Misc improvements of record package in HOL.
* December 2007: Florian Haftmann, TUM
Overloading and class instantiation target.
* December 2007: Florian Haftmann, TUM
New version of primrec package for local theories.
* December 2007: Alexander Krauss, TUM
Method "induction_scheme" in HOL.
* November 2007: Peter Lammich, Uni Muenster
HOL-Lattice: some more lemmas.
Contributions to Isabelle2007
-----------------------------
* October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
State Spaces: The Locale Way (in HOL).
* October 2007: Mark A. Hillebrand, DFKI
Robust sub/superscripts in LaTeX document output.
* August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
HOL-Word: a library for fixed-size machine words in Isabelle.
* August 2007: Brian Huffman, PSU
HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
* June 2007: Amine Chaieb, TUM
Semiring normalization and Groebner Bases.
Support for dense linear orders.
* June 2007: Joe Hurd, Oxford
Metis theorem-prover.
* 2007: Kong W. Susanto, Cambridge
HOL: Metis prover integration.
* 2007: Stefan Berghofer, TUM
HOL: inductive predicates and sets.
* 2007: Norbert Schirmer, TUM
HOL/record: misc improvements.
* 2006/2007: Alexander Krauss, TUM
HOL: function package and related theories on termination.
* 2006/2007: Florian Haftmann, TUM
Pure: generic code generator framework.
Pure: class package.
HOL: theory reorganization, code generator setup.
* 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
Julien Narboux, TUM
HOL/Nominal package and related tools.
* November 2006: Lukas Bulwahn, TUM
HOL: method "lexicographic_order" for function package.
* October 2006: Stefan Hohe, TUM
HOL-Algebra: ideals and quotients over rings.
* August 2006: Amine Chaieb, TUM
Experimental support for generic reflection and reification in HOL.
* July 2006: Rafal Kolanski, NICTA
Hex (0xFF) and binary (0b1011) numerals.
* May 2006: Klaus Aehlig, LMU
Command 'normal_form': normalization by evaluation.
* May 2006: Amine Chaieb, TUM
HOL-Complex: Ferrante and Rackoff Algorithm for linear real
arithmetic.
* February 2006: Benjamin Porter, NICTA
HOL and HOL-Complex: generalised mean value theorem, continuum is
not denumerable, harmonic and arithmetic series, and denumerability
of rationals.
* October 2005: Martin Wildmoser, TUM
Sketch for Isar 'guess' element.
Contributions to Isabelle2005
-----------------------------
* September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
HOL-Complex: Formalization of Taylor series.
* September 2005: Stephan Merz, Alwen Tiu, QSL Loria
Components for SAT solver method using zChaff.
* September 2005: Ning Zhang and Christian Urban, LMU Munich
A Chinese theory.
* September 2005: Bernhard Haeupler, TUM
Method comm_ring for proving equalities in commutative rings.
* July/August 2005: Jeremy Avigad, Carnegie Mellon University
Various improvements of the HOL and HOL-Complex library.
* July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
Some structured proofs about completeness of real numbers.
* May 2005: Rafal Kolanski and Gerwin Klein, NICTA
Improved retrieval of facts from theory/proof context.
* February 2005: Lucas Dixon, University of Edinburgh
Improved subst method.
* 2005: Brian Huffman, OGI
Various improvements of HOLCF.
Some improvements of the HOL-Complex library.
* 2005: Claire Quigley and Jia Meng, University of Cambridge
Some support for asynchronous communication with external provers
(experimental).
* 2005: Florian Haftmann, TUM
Contributions to document 'sugar'.
Various ML combinators, notably linear functional transformations.
Some cleanup of ML legacy.
Additional antiquotations.
Improved Isabelle web site.
* 2004/2005: David Aspinall, University of Edinburgh
Various elements of XML and PGIP based communication with user
interfaces (experimental).
* 2004/2005: Gerwin Klein, NICTA
Contributions to document 'sugar'.
Improved Isabelle web site.
Improved HTML presentation of theories.
* 2004/2005: Clemens Ballarin, TUM
Provers: tools for transitive relations and quasi orders.
Improved version of locales, notably interpretation of locales.
Improved version of HOL-Algebra.
* 2004/2005: Amine Chaieb, TUM
Improved version of HOL presburger method.
* 2004/2005: Steven Obua, TUM
Improved version of HOL/Import, support for HOL-Light.
Improved version of HOL-Complex-Matrix.
Pure/defs: more sophisticated checks on well-formedness of overloading.
Pure/Tools: an experimental evaluator for lambda terms.
* 2004/2005: Norbert Schirmer, TUM
Contributions to document 'sugar'.
Improved version of HOL/record.
* 2004/2005: Sebastian Skalberg, TUM
Improved version of HOL/Import.
Some internal ML reorganizations.
* 2004/2005: Tjark Weber, TUM
SAT solver method using zChaff.
Improved version of HOL/refute.
:maxLineLen=78:
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -1,17191 +1,17196 @@
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
+----------------------------
+
+
+
New in Isabelle2022 (October 2022)
----------------------------------
*** General ***
* The instantiation of schematic goals is now displayed explicitly as a
list of variable assignments. This works for proof state output, and at
the end of a toplevel proof. In rare situations, a proof command or
proof method may violate the intended goal discipline, by not producing
an instance of the original goal, but there is only a warning, no hard
error.
* Session ROOT files support 'chapter_definition' entries (optional).
This allows to associate additional information as follows:
- "chapter_definition NAME (GROUPS)" to make all sessions that belong
to this chapter members of the given groups
- "chapter_definition NAME description TEXT" to provide a description
for presentation purposes
* Old-style {* verbatim *} tokens have been discontinued (legacy feature
since Isabelle2019). INCOMPATIBILITY, use \cartouche\ syntax instead.
*** Isabelle/jEdit Prover IDE ***
* Command 'print_state' outputs a plain message, i.e. "writeln" instead
of "state". Thus it is displayed in the Output panel, even if the option
"editor_output_state" is disabled.
*** Isabelle/VSCode Prover IDE ***
* VSCodium, an open-source distribution of VSCode without MS telemetry,
has been bundled with Isabelle as add-on component. The command-line
tool "isabelle vscode" automatically configures it as Isabelle/VSCode
and starts the application. This includes special support for the
UTF-8-Isabelle encoding and the corresponding Isabelle fonts.
* Command-line tools "isabelle electron" and "isabelle node" provide
access to the underlying technologies of VSCodium, for use in other
applications. This essentially provides a freely programmable Chromium
browser engine that works uniformly on all platforms.
Example:
URL="https://isabelle.in.tum.de" isabelle electron \
--app="$(isabelle getenv -b ISABELLE_HOME)"/src/Tools/Electron/test
*** HTML/PDF presentation ***
* Management of dependencies has become more robust and accurate,
following the session build hierarchy, and the up-to-date notion of
"isabelle build". Changed sessions and updated builds will cause new
HTML presentation, when that is enabled eventually. Unchanged sessions
retain their HTML output that is already present. Thus HTML presentation
for basic sessions like "HOL" and "HOL-Analysis" is produced at most
once, as required by user sessions.
* HTML presentation no longer supports README.html, which was meant as
add-on to the index.html of a session. Rare INCOMPATIBILITY, consider
using a separate theory "README" with Isabelle document markup/markdown.
* ML files (and other auxiliary files) are presented with detailed
hyperlinks, just like regular theory sources.
* Support for external hyperlinks (URLs).
* Support for internal hyperlinks to files that belong formally to the
presented session.
*** HOL ***
* HOL record types: new simproc that sorts update expressions, guarded
by configuration option "record_sort_updates" (default: false). Some
examples are in theory "HOL-Examples.Records".
* More explanations on the new, verified order prover for partial and
linear orders, which first appeared in Isabelle2021-1.
The order prover rearranges the goal to prove False, then retrieves
order literals (i.e. x = y, x <= y, x < y, and their negated versions)
from the premises and finally tries to derive a contradiction. Its main
use case is as a solver to the Simplifier, where it e.g. solves premises
of conditional rewrite rules.
The new prover (src/Provers/order_tac.ML) replaces the old prover
(src/Provers/order.ML) and improves upon the old one in several ways:
- The completeness of the prover is verified in Isabelle (see the ATVA
2021 paper "A Verified Decision Procedure for Orders in
Isabelle/HOL").
- The new prover is complete for partial orders.
- The interface to register new orders was reworked to reduce
boilerplate.
The prover has two configuration attributes that control its behaviour:
- order_trace (default: false) to enable tracing for the solver.
- order_split_limit (default: 8) to limit the number of order literals
of the form ~ x < y that are passed to the solver since those lead
to case splitting and thus exponential runtime. This only applies to
partial orders.
The prover is agnostic to the object-logic, but the default setup is for
HOL: see theory HOL.Orderings with ML structure HOL_Order_Tac. The
structure allows us to register new orders with the functions
HOL_Order_Tac.declare_order and HOL_Order_Tac.declare_linorder. Using
these functions, we register the orders of the type classes order and
linorder with the solver. If possible, one should instantiate these type
classes instead of adding new orders to the solver. One can also
interpret the type class locale as in src/HOL/Library/Sublist.thy, which
contains e.g. the prefix order on lists.
The proof method "order" invokes the prover in a standalone fashion.
The diagnostic command 'print_orders' shows all orders known to the
prover in the current context.
* Meson: added support for polymorphic "using" facts. Minor
INCOMPATIBILITY.
* Moved auxiliary computation constant "divmod_nat" to theory
"HOL.Euclidean_Division". Minor INCOMPATIBILITY.
* Renamed attribute "arith_split" to "linarith_split". Minor
INCOMPATIBILITY.
* Theory "HOL.Rings": rule split_of_bool_asm is not split any longer,
analogously to split_if_asm. INCOMPATIBILITY.
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
* Streamlined primitive definitions of division and modulus on integers.
INCOMPATIBILITY.
* Theory "HOL.Fun":
- Added predicate monotone_on and redefined monotone to be an
abbreviation. Lemma monotone_def is explicitly provided for backward
compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
- Changed argument order of mono_on and strict_mono_on to uniformize
with monotone_on and the general "characterizing set at the beginning
of predicates" preference. Also change them to be abbreviations
of monotone_of. Lemmas mono_on_def and strict_mono_on_def are
explicitly provided for backward compatibility but their usage is
discouraged. INCOMPATIBILITY.
- Move mono, strict_mono, antimono, and relevant lemmas to Fun theory.
Also change them to be abbreviations of mono_on, strict_mono_on,
and monotone, respectively. Lemmas mono_def, strict_mono_def, and
antimono_def are explicitly provided for backward compatibility but
their usage is discouraged. Minor INCOMPATIBILITY.
- Added lemmas.
monotone_onD
monotone_onI
monotone_on_empty[simp]
monotone_on_o
monotone_on_subset
* Theory "HOL.Relation":
- Added predicate reflp_on and redefined reflp to be an abbreviation.
Lemma reflp_def is explicitly provided for backward compatibility
but its usage is discouraged. Minor INCOMPATIBILITY.
- Added predicate totalp_on and abbreviation totalp.
- Replaced HOL.implies by Pure.imp in lemma reflp_mono for consistency
with other lemmas. Minor INCOMPATIBILITY.
- Added lemmas.
preorder.asymp_greater
preorder.asymp_less
reflp_onD
reflp_onI
reflp_on_Inf
reflp_on_Sup
reflp_on_empty[simp]
reflp_on_inf
reflp_on_mono
reflp_on_subset
reflp_on_sup
total_on_subset
totalpD
totalpI
totalp_onD
totalp_onI
totalp_on_empty[simp]
totalp_on_subset
totalp_on_total_on_eq[pred_set_conv]
* Theory "HOL.Transitive_Closure":
- Added lemmas.
total_on_trancl
totalp_on_tranclp
* New theory "HOL-Library.NList" of fixed length lists.
* New Theory "HOL-Library.Code_Abstract_Char" implements characters by
target language integers, sacrificing pattern patching in exchange for
dramatically increased performance for comparisons.
* Theory "HOL-Library.Char_ord": streamlined logical specifications.
Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset":
- Consolidated operation and fact names.
multp ~> multp_code
multeqp ~> multeqp_code
multp_cancel_add_mset ~> multp_cancel_add_mset0
multp_cancel_add_mset0[simplified] ~> multp_cancel_add_mset
multp_code_iff ~> multp_code_iff_mult
multeqp_code_iff ~> multeqp_code_iff_reflcl_mult
Minor INCOMPATIBILITY.
- Moved mult1_lessE out of preorder type class and add explicit
assumption. Minor INCOMPATIBILITY.
- Added predicate multp equivalent to set mult. Reuse name previously
used for what is now called multp_code. Minor INCOMPATIBILITY.
- Lifted multiple lemmas from mult to multp.
- Redefined less_multiset to be based on multp. INCOMPATIBILITY.
- Added lemmas.
Multiset.bex_greatest_element
Multiset.bex_least_element
filter_mset_cong
filter_mset_cong0
image_mset_eq_image_mset_plusD
image_mset_eq_plusD
image_mset_eq_plus_image_msetD
image_mset_filter_mset_swap
monotone_multp_multp_image_mset
monotone_on_multp_multp_image_mset
multp_image_mset_image_msetD
* Theory "HOL-Library.Sublist": added lemma map_mono_strict_suffix.
* Theory "HOL-ex.Sum_of_Powers" has been deleted. The same material is
in the AFP as Bernoulli.
* Session HOL-Algebra: some facts have been renamed to avoid fact name
clashes on interpretation:
is_ring ~> ring_axioms
cring ~> cring_axioms
R_def ~> R_m_def
INCOMPATIBILITY.
* Nitpick: To avoid technical issues, prefer non-JNI solvers to JNI
solvers by default. Minor INCOMPATIBILITY.
* Sledgehammer:
- Redesigned multithreading to provide more fine grained prover
schedules. The binary option 'slice' has been replaced by a numeric
value 'slices' indicating the number of desired slices. Stronger
provers can now be run by more than one thread simultaneously. The
new option 'max_proofs' controls the number of proofs shown.
INCOMPATIBILITY.
- Introduced sledgehammer_outcome data type and changed return type of
ML function Sledgehammer.run_sledgehammer from "bool * (string *
string list)" to "bool * (sledgehammer_outcome * string)". The
former value can be recomputed with "apsnd (ATP_Util.map_prod
Sledgehammer.short_string_of_sledgehammer_outcome single)".
INCOMPATIBILITY.
- Added support for TX0 and TX1 TPTP formats and $ite/$let expressions
in TH0 and TH1.
- Added support for cvc5.
- Generate Isar proofs by default when and only when the one-liner
proof fails to replay and the Isar proof succeeds.
- Replaced option "sledgehammer_atp_dest_dir" by
"sledgehammer_atp_problem_dest_dir", for problem files, and
"sledgehammer_atp_proof_dest_dir", for proof files. Minor
INCOMPATIBILITY.
- Removed support for experimental prover 'z3_tptp'.
- The fastest successfully preplayed proof is always suggested.
- All SMT solvers but Z3 now resort to suggest (smt (verit)) when no
proof could be preplayed.
- Added new "some_preplayed" value to "expect" option to specify that
some successfully preplayed proof is expected. This is in contrast
to the "some" value which doesn't specify whether preplay succeeds
or not.
* Mirabelle:
- Replaced sledgehammer option "keep" by "keep_probs", for problems
files, and "keep_proofs" for proof files. Minor INCOMPATIBILITY.
- Added option "-r INT" to randomize the goals with a given 64-bit
seed before selection.
- Added option "-y" for a dry run.
- Renamed run_action to run in Mirabelle.action record. Minor
INCOMPATIBILITY.
- Run the actions on goals before commands "unfolding" and "using".
* (Co)datatype package:
- BNFs now require a strict cardinality bound (o).
Minor INCOMPATIBILITY for existing manual BNF declarations.
- Lemma map_ident_strong is now generated for all BNFs.
* More ambitious minimization of case expressions in generated code.
* Code generation for Scala: type annotations in pattern bindings are
printed in a way suitable for Scala 3.
*** ML ***
* Type Bytes.T supports scalable byte strings, beyond the limit of
String.maxSize (approx. 64 MB on 64_32 architecture).
* Operations for XZ compression (via Isabelle/Scala):
XZ.compress: Bytes.T -> Bytes.T
XZ.uncompress: Bytes.T -> Bytes.T
*** System ***
* Isabelle/Scala is now based on Scala 3. This is a completely different
compiler ("dotty") and a quite different source language (we are using
the classic Java-style syntax, not the new Python-style syntax).
Occasional INCOMPATIBILITY, see also the official Scala documentation
https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
* External Isabelle tools implemented as .scala scripts are no longer
supported. INCOMPATIBILITY, instead provide a proper Isabelle/Scala
module with etc/build.props and "services" for a suitable class instance
of isabelle.Isabelle_Scala_Tools. For example, see
$ISABELLE_HOME/etc/build.props and its isabelle.Tools, which defines the
standard Isabelle tools.
* The session build database now maintains an additional "uuid" column
to identity the original build process uniquely. Thus other tools may
dependent symbolically on a particular build instance.
* Command-line tool "isabelle build_docker" supports Docker within Snap
more robustly; see also option -W.
* Command-line tool "isabelle scala_project" supports Gradle as
alternative to Maven: either option -G or -M needs to be specified
explicitly. This increases the chances that the Java/Scala IDE project
works properly.
* Command-line tool "isabelle hg_sync" synchronizes the working
directory of a local Mercurial repository with a target directory, using
rsync notation for destinations.
* Command-line tool "isabelle sync" synchronizes Isabelle + AFP
repositories with a target directory, based on "isabelle hg_sync". Local
jars and sessions images may be uploaded as well, to avoid redundant
builds on the remote side. This tool requires a Mercurial clone of the
Isabelle repository: a regular download of the distribution will not
work!
* Command-line tool "isabelle log" has been refined to support multiple
sessions, and to match messages against regular expressions (using Java
Pattern syntax).
* System option "show_states" controls output of toplevel command states
(notably proof states) in batch-builds; in interactive mode this is
always done on demand. The option is relevant for tools that operate on
exported PIDE markup, e.g. document presentation or diagnostics. For
example:
isabelle build -o show_states FOL-ex
isabelle log -v -U FOL-ex
Option "show_states" is also the default for the configuration option
"show_results" within the formal context.
Note that printing intermediate states may cause considerable slowdown
in building a session.
* Session ROOT entries support 'export_classpath' to augment the
Java/Scala name space for tools that allow dynamic loading of service
classes within a session context. A notable example is document
preparation, which works via the class isabelle.Document_Build.Engine
and is configured by the corresponding system option "document_build".
The Isabelle/Isar command 'scala_build_generated_files' helps to produce
a suitable .jar module for inclusion via 'export_classpath'.
* Isabelle/Scala SSH connections now use regular OpenSSH executables
from the local system: ssh, scp, sftp; the old ssh-java component has
been discontinued. This has various practical consequences:
- Authentication and configuration works accurately via the official
.ssh/known_hosts and .ssh/config files.
- Host connections are usually shared (via multiplexed channels), to
reduce the overhead for multiple commands. This also works for SSH
connections for rsync (e.g. "isabelle sync"). Windows/Cygwin does
not support multiplexing: the functionality should be the same, but
slower, with a new connection for each command.
- Multiple hops via "bastion hosts" can be easily configured in
.ssh/config via ProxyJump declarations. The former Isabelle/Scala
parameters for proxy_host etc. have been discontinued: minor
INCOMPATIBILITY.
* The MLton compiler for x86_64-linux has been bundled as Isabelle
component, since Ubuntu 22.04 no longer provides a suitable package.
Note that on macOS, MLton is readily available via Homebrew:
https://formulae.brew.sh/formula/mlton
The Isabelle settings refer to an executable "$ISABELLE_MLTON" and
command-line options $ISABELLE_MLTON_OPTIONS, which need to fit
together. Potential INCOMPATIBILITY for existing
$ISABELLE_HOME_USER/etc/settings.
New in Isabelle2021-1 (December 2021)
-------------------------------------
*** General ***
* The Isabelle/Haskell library ($ISABELLE_HOME/src/Tools/Haskell) has
been significantly improved. In particular, module Isabelle.Bytes
provides type Bytes for light-weight byte strings (with optional UTF8
interpretation), similar to type string in Isabelle/ML. Isabelle symbols
now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs.
Isabelle/Scala/PIDE.
* Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
in interactive mode, but it could occasionally cause unnecessary
slowdown. It can be disabled like this:
context notes [[show_results = false]]
begin
definition "test = True"
theorem test by (simp add: test_def)
end
* Theory_Data / Generic_Data: "val extend = I" has been removed;
obsolete since Isabelle2021.
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.
*** Isar ***
* Commands 'syntax' and 'no_syntax' now work in a local theory context,
but in contrast to 'notation' and 'no_notation' there is no proper way
to refer to local entities. Note that local syntax works well with
'bundle', e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory
Main of Isabelle/HOL.
* The improper proof command 'guess' is no longer part of by Pure, but
provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY,
existing applications need to import session "Pure-ex" and theory
"Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess'
command, using explicit 'obtain' instead.
* More robust 'proof' outline for method "induct": support nested cases.
*** Isabelle/jEdit Prover IDE ***
* The main plugin for Isabelle/jEdit can be deactivated and reactivated
as documented --- was broken at least since Isabelle2018.
* Isabelle/jEdit is now composed more conventionally from the original
jEdit text editor in $JEDIT_HOME (with minor patches), plus two Isabelle
plugins that are produced in $JEDIT_SETTINGS/jars on demand. The main
isabelle.jedit module is now part of Isabelle/Scala (as one big
$ISABELLE_SCALA_JAR).
* Add-on components may provide their own jEdit plugins, via the new
Scala/Java module concept: instances of class
isabelle.Scala_Project.Plugin that are declared as "services" within
etc/build.props are activated on Isabelle/jEdit startup. E.g. see
existing isabelle.jedit.JEdit_Plugin0 (for isabelle_jedit_base.jar) and
isabelle.jedit.JEdit_Plugin1 (for isabelle_jedit_main.jar).
* Support for built-in font substitution of jEdit text area.
*** Document preparation ***
* HTML presentation now includes links to formal entities.
* High-quality blackboard-bold symbols from font "txmia" (LaTeX package
"pxfonts"): \\\\\\\\\\\\\\\\\\\\\\\\\\.
* More predefined symbols: \ \ \ (package "stmaryrd"), \ \ (LaTeX
package "pifont").
* Document antiquotations for ML text have been refined: "def" and "ref"
variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
type arguments for constructors (only relevant for index), e.g.
@{ML_type \'a list\} vs. @{ML_type 'a \list\}; @{ML_op} has been renamed
to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax.
* Option "document_logo" determines if an instance of the Isabelle logo
should be created in the document output directory. The given string
specifies the name of the logo variant, while "_" (underscore) refers to
the unnamed variant. The output file name is always "isabelle_logo.pdf".
* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:
- "lualatex" (default): use ISABELLE_LUALATEX for a standard LaTeX
build with optional ISABELLE_BIBTEX and ISABELLE_MAKEINDEX
- "pdflatex": as above, but use ISABELLE_PDFLATEX (legacy mode for
special LaTeX styles)
- "build": delegate to the executable "./build pdf"
The presence of a "build" command within the document output directory
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
* Option "document_comment_latex" enables regular LaTeX comment.sty,
instead of the historic version for plain TeX (default). The latter is
much faster, but in conflict with LaTeX classes like Dagstuhl LIPIcs.
* Option "document_echo" informs about document file names during
session presentation.
* Option "document_heading_prefix" specifies a prefix for the LaTeX
macro names generated from document heading commands like 'chapter',
'section' etc. The default is "isamarkup", so 'section' becomes
"\isamarkupsection" for example.
* The command-line tool "isabelle latex" has been discontinued,
INCOMPATIBILITY for old document build scripts.
- Former "isabelle latex -o sty" has become obsolete: Isabelle .sty
files are automatically generated within the document output
directory.
- Former "isabelle latex -o pdf" should be replaced by
"$ISABELLE_LUALATEX root" or "$ISABELLE_PDFLATEX root" (without
quotes), according to the intended LaTeX engine.
- Former "isabelle latex -o bbl" should be replaced by
"$ISABELLE_BIBTEX root" (without quotes).
- Former "isabelle latex -o idx" should be replaced by
"$ISABELLE_MAKEINDEX root" (without quotes).
* Option "document_bibliography" explicitly enables the use of bibtex;
the default is to check the presence of root.bib, but it could have a
different name.
* Improved LaTeX typesetting of \...\ using \guilsinglleft ...
\guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
(which is now also the default in "isabelle mkroot").
* Simplified typesetting of \...\ using \guillemotleft ...
\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
no longer required.
*** Pure ***
* "global_interpretation" is applicable in instantiation and overloading
targets and in any nested target built on top of a target supporting
"global_interpretation".
*** HOL ***
* New order prover.
* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant
potential for change can be avoided if interpretations of type class
"order" are replaced or augmented by interpretations of locale
"ordering".
* Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor
INCOMPATIBILITY; note that for most applications less elementary lemmas
exists.
* Lemma "permutes_induct" has been given stronger hypotheses and named
premises. INCOMPATIBILITY.
* Combinator "Fun.swap" resolved into a mere input abbreviation in
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in
bundle bit_operations_syntax. INCOMPATIBILITY.
* Bit operations set_bit, unset_bit and flip_bit are now class
operations. INCOMPATIBILITY.
* Simplified class hierarchy for bit operations: bit operations reside
in classes (semi)ring_bit_operations, class semiring_bit_shifts is gone.
* Consecutive conversions to and from words are not collapsed in any
case: rules unsigned_of_nat, unsigned_of_int, signed_of_int,
signed_of_nat, word_of_nat_eq_0_iff, word_of_int_eq_0_iff are not simp
by default any longer. INCOMPATIBILITY.
* Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
"setBit", "clearBit". See there further the changelog in theory Guide.
INCOMPATIBILITY.
* Reorganized classes and locales for boolean algebras. INCOMPATIBILITY.
* New simp rules: less_exp, min.absorb1, min.absorb2, min.absorb3,
min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor
INCOMPATIBILITY.
* The Mirabelle testing tool is now part of Main HOL, and accessible via
the command-line tool "isabelle mirabelle" (implemented in
Isabelle/Scala). It has become more robust and supports parallelism
within Isabelle/ML.
* Nitpick: External solver "MiniSat" is available for all supported
Isabelle platforms (including 64bit Windows and ARM); while
"MiniSat_JNI" only works for Intel Linux and macOS.
* Nitpick/Kodkod: default is back to external Java process (option
kodkod_scala = false), both for PIDE and batch builds. This reduces
confusion and increases robustness of timeouts, despite substantial
overhead to run an external JVM. For more fine-grained control, the
kodkod_scala option can be modified within the formal theory context
like this:
declare [[kodkod_scala = false]]
* Sledgehammer:
- Update of bundled provers:
. E 2.6
. Vampire 4.6 (with Open Source license)
. veriT 2021.06.1-rmx
. Zipperposition 2.1
. Z3 4.4.1 for arm64-linux, which approximates Z3 4.4.0pre,
but sometimes fails or crashes
- Adjusted default provers:
cvc4 vampire verit e spass z3 zipperposition
- Adjusted Zipperposition's slicing.
- Removed legacy "lam_lifting" (synonym for "lifting") from option
"lam_trans". Minor INCOMPATIBILITY.
- Renamed "hide_lams" to "opaque_lifting" in option "lam_trans". Minor
INCOMPATIBILITY.
- Added "opaque_combs" to option "lam_trans": lambda expressions are
rewritten using combinators, but the combinators are kept opaque,
i.e. without definitions.
* Metis:
- Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
- Updated the Metis prover underlying the "metis" proof method to
version 2.4 (release 20200713). The new version fixes one
implementation defect. Very slight INCOMPATIBILITY.
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in
a global theory via 'unbundle'. The opposite declarations are bundled as
"no_lattice_syntax". Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
use explict expression instead. Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": consolidated abbreviations Mempty,
Melem, not_Melem to empty_mset, member_mset, not_member_mset
respectively. Minor INCOMPATIBILITY.
* Theory "HOL-Library.Multiset": consolidated operation and fact names:
inf_subset_mset ~> inter_mset
sup_subset_mset ~> union_mset
multiset_inter_def ~> inter_mset_def
sup_subset_mset_def ~> union_mset_def
multiset_inter_count ~> count_inter_mset
sup_subset_mset_count ~> count_union_mset
* Theory "HOL-Library.Complex_Order": Defines less, less_eq on complex
numbers. Not imported by default.
* Theory "HOL-Library.Multiset": syntax precendence for membership
operations has been adjusted to match the corresponding precendences on
sets. Rare INCOMPATIBILITY.
* Theory "HOL-Library.Cardinality": code generator setup based on the
type classes finite_UNIV and card_UNIV has been moved to
"HOL-Library.Code_Cardinality", to avoid incompatibilities with
other code setups for sets in AFP/Containers. Applications relying on
this code setup should import "HOL-Library.Code_Cardinality". Minor
INCOMPATIBILITY.
* Theory "HOL-Library.Permutation" has been renamed to the more specific
"HOL-Library.List_Permutation". Note that most notions from that theory
are already present in theory "HOL-Combinatorics.Permutations".
INCOMPATIBILITY.
* Dedicated session "HOL-Combinatorics". INCOMPATIBILITY: theories
"Permutations", "List_Permutation" (formerly "Permutation"), "Stirling",
"Multiset_Permutations", "Perm" have been moved there from session
HOL-Library.
* Theory "HOL-Combinatorics.Transposition" provides elementary swap
operation "transpose".
* Theory "HOL-Analysis.Infinite_Sum": new theory for infinite sums with
a more general definition than the existing theory Infinite_Set_Sum.
(Infinite_Set_Sum contains theorems relating the two definitions.)
* Theory "HOL-Analysis.Product_Vector": Instantiation of the product of
uniform spaces as a uniform space. Minor INCOMPATIBILITY: the old
definition "uniformity_prod_def" is available as a derived fact
"uniformity_dist".
* Session "HOL-Analysis" and "HOL-Probability": indexed products of
discrete distributions, negative binomial distribution, Hoeffding's
inequality, Chernoff bounds, Cauchy–Schwarz inequality for nn_integral,
and some more small lemmas. Some theorems that were stated awkwardly
before were corrected. Minor INCOMPATIBILITY.
* Session "HOL-Analysis": the complex Arg function has been identified
with the function "arg" of Complex_Main, renaming arg ~> Arg also in the
names of arg_bounded. Minor INCOMPATIBILITY.
* Session "HOL-Statespace": various improvements and cleanup.
*** ML ***
* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.
The main Isabelle/ML interface is Isabelle_System.bash_process with
result type Process_Result.T (resembling class Process_Result in Scala);
derived operations Isabelle_System.bash and Isabelle_System.bash_output
provide similar functionality as before. The underlying TCP/IP server
within Isabelle/Scala is available to other programming languages as
well, notably Isabelle/Haskell.
Rare INCOMPATIBILITY due to subtle semantic differences:
- Processes invoked from Isabelle/ML actually run in the context of
the Java VM of Isabelle/Scala. The settings environment and current
working directory are usually the same on both sides, but there can be
subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML).
- Output via stdout and stderr is line-oriented: Unix vs. Windows
line-endings are normalized towards Unix; presence or absence of a
final newline is irrelevant. The original lines are available as
Process_Result.out_lines/err_lines; the concatenated versions
Process_Result.out/err *omit* a trailing newline (using
Library.trim_line, which was occasional seen in applications before,
but is no longer necessary).
- Output needs to be plain text encoded in UTF-8: Isabelle/Scala
recodes it temporarily as UTF-16. This works for well-formed Unicode
text, but not for arbitrary byte strings. In such cases, the bash
script should write tempory files, managed by Isabelle/ML operations
like Isabelle_System.with_tmp_file to create a file name and
File.read to retrieve its content.
- The Isabelle/Scala "bash_process" server requires a PIDE session
context. This could be a regular batch session (e.g. "isabelle
build"), a PIDE editor session (e.g. "isabelle jedit"), or headless
PIDE (e.g. "isabelle dump" or "isabelle server"). Note that old
"isabelle console" or raw "isabelle process" don't have that.
New Process_Result.timing works as in Isabelle/Scala, based on direct
measurements of the bash_process wrapper in C: elapsed time is always
available, CPU time is only available on Linux and macOS, GC time is
unavailable.
* The following Isabelle/ML system operations are run in the context of
Isabelle/Scala, within a PIDE session context:
- Isabelle_System.make_directory
- Isabelle_System.copy_dir
- Isabelle_System.copy_file
- Isabelle_System.copy_base_file
- Isabelle_System.rm_tree
- Isabelle_System.download
* Term operations under abstractions are now more robust (and more
strict) by using the formal proof context in subsequent operations:
Variable.dest_abs
Variable.dest_abs_cterm
Variable.dest_all
Variable.dest_all_cterm
This works under the assumption that terms are always properly declared
to the proof context (e.g. via Variable.declare_term). Failure to do so,
or working with the wrong context, will cause an error (exception Fail,
based on Term.USED_FREE from Term.dest_abs_fresh).
The Simplifier and equational conversions now use the above operations
routinely, and thus require user-space tools to be serious about the
proof context (notably in their use of Goal.prove, SUBPROOF etc.).
INCOMPATIBILITY in add-on tools is to be expected occasionally: a proper
context discipline needs to be followed.
* Former operations Term.dest_abs and Logic.dest_all (without a proper
context) have been discontinued. INCOMPATIBILITY, either use
Variable.dest_abs etc. above, or the following operations that imitate
the old behavior to a great extent:
Term.dest_abs_global
Logic.dest_all_global
This works under the assumption that the given (sub-)term directly shows
all free variables that need to be avoided when generating a fresh name.
A violation of the assumption are variables stemming from the enclosing
context that get involved in a proof only later.
* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
operations to accumulate items from types and terms, using a fast
syntactic order. The original order of occurrences may be recovered as
well, e.g. via TFrees.list_set.
* Thm.instantiate, Thm.generalize and related operations (e.g.
Variable.import) now use scalable data structures from structure TVars,
Vars, Names etc. INCOMPATIBILITY: e.g. use TVars.empty and TVars.make
for immediate adoption; better use TVars.add, TVars.add_tfrees etc. for
scalable accumulation of items.
* Thm.instantiate_beta applies newly emerging abstractions to their
arguments in the term, but leaves other beta-redexes unchanged --- in
contrast to Drule.instantiate_normalize.
* ML antiquotation "instantiate" allows to instantiate formal entities
(types, terms, theorems) with values given ML. This works uniformly for
"typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a
keyword after the instantiation.
A mode "(schematic)" behind the keyword means that some variables may
remain uninstantiated (fixed in the specification and schematic in the
result); by default, all variables need to be instantiated.
Newly emerging abstractions are applied to their arguments in the term
(using Thm.instantiate_beta).
Examples in HOL:
fun make_assoc_type (A, B) =
\<^instantiate>\'a = A and 'b = B in typ \('a \ 'b) list\\;
val make_assoc_list =
map (fn (x, y) =>
\<^instantiate>\'a = \fastype_of x\ and 'b = \fastype_of y\ and
x and y in term \(x, y)\ for x :: 'a and y :: 'b\);
fun symmetry x y =
\<^instantiate>\'a = \Thm.ctyp_of_cterm x\ and x and y in
lemma \x = y \ y = x\ for x y :: 'a by simp\
fun symmetry_schematic A =
\<^instantiate>\'a = A in
lemma (schematic) \x = y \ y = x\ for x y :: 'a by simp\
* ML antiquotation for embedded lemma supports local fixes, as usual in
many other Isar language elements. For example:
@{lemma "x = x" for x :: nat by (rule refl)}
* ML antiquotations for type constructors and term constants:
\<^Type>\c\
\<^Type>\c T \\ \ \same with type arguments\
\<^Type_fn>\c T \\ \ \fn abstraction, failure via exception TYPE\
\<^Const>\c\
\<^Const>\c T \\ \ \same with type arguments\
\<^Const>\c for t \\ \ \same with term arguments\
\<^Const_>\c \\ \ \same for patterns: case, let, fn\
\<^Const_fn>\c T \\ \ \fn abstraction, failure via exception TERM\
The type/term arguments refer to nested ML source, which may contain
antiquotations recursively. The following argument syntax is supported:
- an underscore (dummy pattern)
- an atomic item of "embedded" syntax, e.g. identifier or cartouche
- an antiquotation in control-symbol/cartouche form, e.g. \<^Type>\c\
as short form of \\<^Type>\c\\.
Examples in HOL:
val natT = \<^Type>\nat\;
fun mk_funT (A, B) = \<^Type>\fun A B\;
val dest_funT = \<^Type_fn>\fun A B => \(A, B)\\;
fun mk_conj (A, B) = \<^Const>\conj for A B\;
val dest_conj = \<^Const_fn>\conj for A B => \(A, B)\\;
fun mk_eq T (t, u) = \<^Const>\HOL.eq T for t u\;
val dest_eq = \<^Const_fn>\HOL.eq T for t u => \(T, (t, u))\\;
* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
corresponding functions for the object-logic of the ML compilation
context. This supersedes older mk_Trueprop / dest_Trueprop operations.
* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
For example:
- type 'a Symtab.table etc.: build
- type 'a Names.table etc.: build
- type 'a list: build and build_rev
- type Buffer.T: build and build_content
For example, see src/Pure/PIDE/xml.ML:
val content_of = Buffer.build_content o fold add_content;
* ML antiquotations \<^try>\expr\ and \<^can>\expr\ operate directly on
the given ML expression, in contrast to functions "try" and "can" that
modify application of a function.
* ML antiquotations for conditional ML text:
\<^if_linux>\...\
\<^if_macos>\...\
\<^if_windows>\...\
\<^if_unix>\...\
* ML profiling has been updated and reactivated, after some degration in
Isabelle2021:
- "isabelle build -o threads=1 -o profiling=..." works properly
within the PIDE session context;
- "isabelle profiling_report" now uses the session build database
(like "isabelle log");
- output uses non-intrusive tracing messages, instead of warnings.
*** System ***
* Almost complete support for arm64-linux platform. The reference
platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
* Update to OpenJDK 17: the current long-term support version of Java.
* Update to Poly/ML 5.9 with improved support for ARM on Linux. On
macOS, the Intel version works more smoothly with Rosetta 2, as already
used in Isabelle2021. Further changes to Poly/ML are documented here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2021-May/002451.html
* Perl is no longer required by Isabelle proper, and no longer provided
by specific Isabelle execution environments (Docker, Cygwin on Windows).
Minor INCOMPATIBILITY, add-on applications involving perl need to
provide it by different means. (Note that proper Isabelle systems
programming works via Scala/Java, without perl, python, ruby etc.).
* Each Isabelle component may specify a Scala/Java jar module
declaratively via etc/build.props (file names are relative to the
component directory). E.g. see $ISABELLE_HOME/etc/build.props with
further explanations in the "system" manual.
* Command-line tool "isabelle scala_build" allows to invoke the build
process of all Scala/Java modules explicitly. Normally this is done
implicitly on demand, e.g. for "isabelle scala" or "isabelle jedit".
* Command-line tool "isabelle scala_project" is has been improved in
various ways:
- sources from all components with etc/build.props are included,
- sources of for the jEdit text editor and the Isabelle/jEdit
plugins (jedit_base and jedit_main) are included by default,
- more sources may be given on the command-line,
- options -f and -D make the tool more convenient,
- Gradle has been replaced by Maven (less ambitious and more robust).
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
managed via Isabelle/Scala instead of perl; the dependency on
libwww-perl has been eliminated (notably on Linux). Rare
INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties
https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
* System options may declare an implicit standard value, which is used
when the option is activated without providing an explicit value, e.g.
"isabelle build -o document -o document_output" instead of
"isabelle build -o document=true -o document_output=output". For options
of type "bool", the standard is always "true" and cannot be specified
differently.
* System option "document=true" is an alias for "document=pdf", and
"document=false" is an alias for "document=" (empty string).
* System option "system_log" specifies an optional log file for internal
messages produced by Output.system_message in Isabelle/ML; the standard
value "-" refers to console progress of the build job. This works for
"isabelle build" or any derivative of it.
* Command-line tool "isabelle version" supports repository archives
(without full .hg directory). It also provides more options.
* Obsolete settings variable ISABELLE_PLATFORM32 has been discontinued.
Note that only Windows supports old 32 bit executables, via settings
variable ISABELLE_WINDOWS_PLATFORM32. Everything else should be
ISABELLE_PLATFORM64 (generic Posix) or ISABELLE_WINDOWS_PLATFORM64
(native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon).
* Timeouts for Isabelle/ML tools are subject to system option
"timeout_scale", to support adjustments to slow machines. Before,
timeout_scale was only used for the overall session build process, now
it affects the underlying Timeout.apply in Isabelle/ML as well. It
treats a timeout specification 0 as "no timeout", instead of "immediate
timeout". Rare INCOMPATIBILITY in boundary cases.
New in Isabelle2021 (February 2021)
-----------------------------------
*** General ***
* On macOS, the IsabelleXYZ.app directory layout now follows the other
platforms, without indirection via Contents/Resources/. INCOMPATIBILITY,
use e.g. IsabelleXYZ.app/bin/isabelle instead of former
IsabelleXYZ.app/Isabelle/bin/isabelle or
IsabelleXYZ.app/Isabelle/Contents/Resources/IsabelleXYZ/bin/isabelle.
* HTML presentation uses rich markup produced by Isabelle/PIDE,
resulting in more colors and links.
* HTML presentation includes auxiliary files (e.g. ML) for each theory.
* Proof method "subst" is confined to the original subgoal range: its
included distinct_subgoals_tac no longer affects unrelated subgoals.
Rare INCOMPATIBILITY.
* Theory_Data extend operation is obsolete and needs to be the identity
function; merge should be conservative and not reset to the empty value.
Subtle INCOMPATIBILITY and change of semantics (due to
Theory.join_theory from Isabelle2020). Special extend/merge behaviour at
the begin of a new theory can be achieved via Theory.at_begin.
*** Isabelle/jEdit Prover IDE ***
* Improved GUI look-and-feel: the portable and scalable "FlatLaf Light"
is used by default on all platforms (appearance similar to IntelliJ
IDEA).
* Improved markup for theory header imports: hyperlinks for theory files
work without formal checking of content.
* The prover process can download auxiliary files (e.g. 'ML_file') for
theories with remote URL. This requires the external "curl" program.
* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
of the formal entity at the caret position.
* The visual feedback on caret entity focus is normally restricted to
definitions within the visible text area. The keyboard modifier "CS"
overrides this: then all defining and referencing positions are shown.
See also option "jedit_focus_modifier".
* The jEdit status line includes widgets both for JVM and ML heap usage.
Ongoing ML ongoing garbage collection is shown as "ML cleanup".
* The Monitor dockable provides buttons to request a full garbage
collection and sharing of live data on the ML heap. It also includes
information about the Java Runtime system.
* PIDE support for session ROOTS: markup for directories.
* Update to jedit-5.6.0, the latest release. This version works properly
on macOS by default, without the special MacOSX plugin.
* Action "full-screen-mode" (shortcut F11 or S+F11) has been modified
for better approximate window size on macOS and Linux/X11.
* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode,
but non-native look-and-feel (FlatLaf).
* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
viewer, instead of re-using the jEdit text editor.
* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical
Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
.ftl.tex extension. The corresponding Naproche-SAD server process can be
disabled by setting the system option naproche_server=false and
restarting the Isabelle application.
*** Document preparation ***
* Keyword 'document_theories' within ROOT specifies theories from other
sessions that should be included in the generated document source
directory. This does not affect the generated session.tex: \input{...}
needs to be used separately.
* The standard LaTeX engine is now lualatex, according to settings
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
pdflatex, but text encoding needs to conform strictly to utf8. Rare
INCOMPATIBILITY.
* Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
document output is always PDF.
* Antiquotation @{tool} refers to Isabelle command-line tools, with
completion and formal reference to the source (external script or
internal Scala function).
* Antiquotation @{bash_function} refers to GNU bash functions that are
checked within the Isabelle settings environment.
* Antiquotations @{scala}, @{scala_object}, @{scala_type},
@{scala_method} refer to checked Isabelle/Scala entities.
*** Pure ***
* Session Pure-Examples contains notable examples for Isabelle/Pure
(former entries of HOL-Isar_Examples).
* Named contexts (locale and class specifications, locale and class
context blocks) allow bundle mixins for the surface context. This allows
syntax notations to be organized within bundles conveniently. See theory
"HOL-ex.Specifications_with_bundle_mixins" for examples and the isar-ref
manual for syntax descriptions.
* Definitions in locales produce rule which can be added as congruence
rule to protect foundational terms during simplification.
* Consolidated terminology and function signatures for nested targets:
- Local_Theory.begin_nested replaces Local_Theory.open_target
- Local_Theory.end_nested replaces Local_Theory.close_target
- Combination of Local_Theory.begin_nested and
Local_Theory.end_nested(_result) replaces
Local_Theory.subtarget(_result)
INCOMPATIBILITY.
* Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY.
*** HOL ***
* Session HOL-Examples contains notable examples for Isabelle/HOL
(former entries of HOL-Isar_Examples, HOL-ex etc.).
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.
* Zipperposition 2.0 is now included as Isabelle component for
experimentation, e.g. in "sledgehammer [prover = zipperposition]".
* Sledgehammer:
- support veriT in proof preplay
- take adventage of more cores in proof preplay
* Updated the Metis prover underlying the "metis" proof method to
version 2.4 (release 20180810). The new version fixes one soundness
defect and two incompleteness defects. Very slight INCOMPATIBILITY.
* Nitpick/Kodkod may be invoked directly within the running
Isabelle/Scala session (instead of an external Java process): this
improves reactivity and saves resources. This experimental feature is
guarded by system option "kodkod_scala" (default: true in PIDE
interaction, false in batch builds).
* Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
INCOMPATIBILITY, consider repairing proofs locally like this:
supply subst_all [simp del] [[simproc del: defined_all]]
* Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
on datatypes to "False" if either side is a proper subexpression of the
other (for any datatype with a reasonable size function).
* Syntax for state monad combinators fcomp and scomp is organized in
bundle state_combinator_syntax. Minor INCOMPATIBILITY.
* Syntax for reflected term syntax is organized in bundle term_syntax,
discontinuing previous locale term_syntax. Minor INCOMPATIBILITY.
* New constant "power_int" for exponentiation with integer exponent,
written as "x powi n".
* Added the "at most 1" quantifier, Uniq.
* For the natural numbers, "Sup {} = 0".
* New constant semiring_char gives the characteristic of any type of
class semiring_1, with the convenient notation CHAR('a). For example,
CHAR(nat) = CHAR(int) = CHAR(real) = 0, CHAR(17) = 17.
* HOL-Computational_Algebra.Polynomial: Definition and basic properties
of algebraic integers.
* Library theory "Bit_Operations" with generic bit operations.
* Library theory "Signed_Division" provides operations for signed
division, instantiated for type int.
* Theory "Multiset": removed misleading notation \# for sum_mset;
replaced with \\<^sub>#. Analogous notation for prod_mset also exists now.
* New theory "HOL-Library.Word" takes over material from former session
"HOL-Word". INCOMPATIBILITY: need to adjust imports.
* Theory "HOL-Library.Word": Type word is restricted to bit strings
consisting of at least one bit. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Bit operations NOT, AND, OR, XOR are based
on generic algebraic bit operations from theory
"HOL-Library.Bit_Operations". INCOMPATIBILITY.
* Theory "HOL-Library.Word": Most operations on type word are set up for
transfer and lifting. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Generic type conversions. INCOMPATIBILITY,
sometimes additional rewrite rules must be added to applications to get
a confluent system again.
* Theory "HOL-Library.Word": Uniform polymorphic "mask" operation for
both types int and word. INCOMPATIBILITY.
* Theory "HOL-Library.Word": Syntax for signed compare operators has
been consolidated with syntax of regular compare operators. Minor
INCOMPATIBILITY.
* Former session "HOL-Word": Various operations dealing with bit values
represented as reversed lists of bools are separated into theory
Reversed_Bit_Lists in session Word_Lib in the AFP. INCOMPATIBILITY.
* Former session "HOL-Word": Theory "Word_Bitwise" has been moved to AFP
entry Word_Lib as theory "Bitwise". INCOMPATIBILITY.
* Former session "HOL-Word": Compound operation "bin_split" simplifies
by default into its components "drop_bit" and "take_bit".
INCOMPATIBILITY.
* Former session "HOL-Word": Operations lsb, msb and set_bit are
separated into theories Least_significant_bit, Most_significant_bit and
Generic_set_bit respectively in session Word_Lib in the AFP.
INCOMPATIBILITY.
* Former session "HOL-Word": Ancient int numeral representation has been
factored out in separate theory "Ancient_Numeral" in session Word_Lib in
the AFP. INCOMPATIBILITY.
* Former session "HOL-Word": Operations "bin_last", "bin_rest",
"bin_nth", "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and
"max_word" are now mere input abbreviations. Minor INCOMPATIBILITY.
* Former session "HOL-Word": Misc ancient material has been factored out
into separate theories and moved to session Word_Lib in the AFP. See
theory "Guide" there for further information. INCOMPATIBILITY.
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
are in working order again, as opposed to outputting "GaveUp" on nearly
all problems.
* Session "HOL-Hoare": concrete syntax only for Hoare triples, not
abstract language constructors.
* Session "HOL-Hoare": now provides a total correctness logic as well.
*** FOL ***
* Added the "at most 1" quantifier, Uniq, as in HOL.
* Simproc "defined_all" and rewrite rule "subst_all" have been changed
as in HOL.
*** ML ***
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
registered Isabelle/Scala functions (of type String => String):
invocation works via the PIDE protocol.
* Path.append is available as overloaded "+" operator, similar to
corresponding Isabelle/Scala operation.
* ML statistics via an external Poly/ML process: this allows monitoring
the runtime system while the ML program sleeps.
*** System ***
* Isabelle server allows user-defined commands via
isabelle_scala_service.
* Update/rebuild external provers on currently supported OS platforms,
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
* The command-line tool "isabelle log" prints prover messages from the
build database of the given session, following the the order of theory
sources, instead of erratic parallel evaluation. Consequently, the
session log file is restricted to system messages of the overall build
process, and thus becomes more informative.
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.
* The command-line tool "isabelle logo" only outputs PDF; obsolete EPS
(for DVI documents) has been discontinued. Former option -n has been
turned into -o with explicit file name. Minor INCOMPATIBILITY.
* The command-line tool "isabelle components" supports new options -u
and -x to manage $ISABELLE_HOME_USER/etc/components without manual
editing of Isabelle configuration files.
* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
session databases. It used to be hard-wired for Isabelle + AFP, but
other projects may now participate on equal terms.
* The command-line tool "isabelle process" now prints output to
stdout/stderr separately and incrementally, instead of just one bulk to
stdout after termination. Potential INCOMPATIBILITY for external tools.
* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).
* Batch-builds via "isabelle build" use a PIDE session with special
protocol: this allows to invoke Isabelle/Scala operations from
Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the
java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
This includes full PIDE markup, if option "build_pide_reports" is
enabled.
* The command-line tool "isabelle build" provides option -P DIR to
produce PDF/HTML presentation in the specified directory; -P: refers to
the standard directory according to ISABELLE_BROWSER_INFO /
ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken
from the build database -- from this or earlier builds with option
document=pdf.
* The command-line tool "isabelle document" generates theory documents
on the spot, using the underlying session build database (exported
LaTeX sources or existing PDF files). INCOMPATIBILITY, the former
"isabelle document" tool was rather different and has been discontinued.
* The command-line tool "isabelle sessions" explores the structure of
Isabelle sessions and prints result names in topological order (on
stdout).
* The Isabelle/Scala "Progress" interface changed slightly and
"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
instead.
* General support for Isabelle/Scala system services, configured via the
shell function "isabelle_scala_service" in etc/settings (e.g. of an
Isabelle component); see implementations of class
Isabelle_System.Service in Isabelle/Scala. This supersedes former
"isabelle_scala_tools" and "isabelle_file_format": minor
INCOMPATIBILITY.
* The syntax of theory load commands (for auxiliary files) is now
specified in Isabelle/Scala, as instance of class
isabelle.Command_Span.Load_Command registered via isabelle_scala_service
in etc/settings. This allows more flexible schemes than just a list of
file extensions. Minor INCOMPATIBILITY, e.g. see theory
HOL-SPARK.SPARK_Setup to emulate the old behaviour.
* JVM system property "isabelle.laf" has been discontinued; the default
Swing look-and-feel is ""FlatLaf Light".
* Isabelle/Phabricator supports Ubuntu 20.04 LTS.
* Isabelle/Phabricator setup has been updated to follow ongoing
development: libphutil has been discontinued. Minor INCOMPATIBILITY:
existing server installations should remove libphutil from
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
directory (e.g. /var/www/phabricator-vcs/libphutil).
* Experimental support for arm64-linux platform. The reference platform
is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
* Support for Apple Silicon, using mostly x86_64-darwin runtime
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
some native arm64-darwin executables (e.g. Java).
New in Isabelle2020 (April 2020)
--------------------------------
*** 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.
* Refined treatment of proof terms, including type-class proofs for
minor object-logics (FOL, FOLP, Sequents).
* The inference kernel is now confined to one main module: structure
Thm, without the former circular dependency on structure Axclass.
* Mixfix annotations may use "' " (single quote followed by space) to
separate delimiters (as documented in the isar-ref manual), without
requiring an auxiliary empty block. A literal single quote needs to be
escaped properly. Minor INCOMPATIBILITY.
*** 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.
* Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
tooltip message popups, corresponding to mouse hovering with/without the
CONTROL/COMMAND key pressed.
* The following actions allow to navigate errors within the current
document snapshot:
isabelle.first-error (CS+a)
isabelle.last-error (CS+z)
isabelle.next-error (CS+n)
isabelle.prev-error (CS+p)
* Support more brackets: \ \ (intended for implicit argument syntax).
* Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
Monitor) applies the jconsole tool on the running Isabelle/jEdit
process. This allows to monitor resource usage etc.
* More adequate default font sizes for Linux on HD / UHD displays:
automatic font scaling is usually absent on Linux, in contrast to
Windows and macOS.
* The default value for the jEdit property "view.antiAlias" (menu item
Utilities / Global Options / Text Area / Anti Aliased smooth text) is
now "subpixel HRGB", instead of former "standard". Especially on Linux
this often leads to faster text rendering, but can also cause problems
with odd color shades. An alternative is to switch back to "standard"
here, and set the following Java system property:
isabelle jedit -Dsun.java2d.opengl=true
This can be made persistent via JEDIT_JAVA_OPTIONS in
$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
application there is a corresponding options file in the same directory.
*** Isabelle/VSCode Prover IDE ***
* Update of State and Preview panels to use new WebviewPanel API of
VSCode.
*** HOL ***
* Improvements of the 'lift_bnf' command:
- Add support for quotient types.
- Generate transfer rules for the lifted map/set/rel/pred constants
(theorems "._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.
* Removed multiplicativity assumption from class
"normalization_semidom". Introduced various new intermediate classes
with the multiplicativity assumption; many theorem statements
(especially involving GCD/LCM) had to be adapted. This allows for a more
natural instantiation of the algebraic typeclasses for e.g. Gaussian
integers. 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" (\)
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-Proofs: build faster thanks to better treatment of proof
terms in Isabelle/Pure.
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor
INCOMPATIBILITY.
* Session HOL-Analysis: proof method "metric" implements a decision
procedure for simple linear statements in metric spaces.
* Session HOL-Complex_Analysis has been split off from HOL-Analysis.
*** 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 Variable.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.
* Prover IDE support for the underlying Poly/ML compiler (not the basis
library). Open $ML_SOURCES/ROOT.ML in Isabelle/jEdit to browse the
implementation with full markup.
*** System ***
* Standard rendering for more Isabelle symbols: \ \ \ \
* 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.
* The command-line tool "isabelle build_docker" has been slightly
improved: it is now properly documented in the "system" manual.
* 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.
* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
"isabelle dump".
* 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 isabelle.Export_Theory in Isabelle/Scala.
* Theory export of structured specifications, based on internal
declarations of Spec_Rules by packages like 'definition', 'inductive',
'primrec', 'function'.
* 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 "\" 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 \cartouche\ 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 \+\ 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>\marker_body\ 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>\contributor arg\ or \<^marker>\license arg\ 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>\tag (proof) name\ 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>\tag name\ 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>\tag \"
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>\cartouche\ notation (e.g. \<^term>\\x y. x\). 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] \\x y. x\}.
*** 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 \, \, \, \ (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 \# 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" = \
module Isabelle.Pure where
allConst, impConst, eqConst :: String
allConst = \\<^const_name>\Pure.all\\
impConst = \\<^const_name>\Pure.imp\\
eqConst = \\<^const_name>\Pure.eq\\
\
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>\abc\ 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>\ARG\.
* 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
"\ \text\", 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 "\ \...\" or "\<^cancel>\...\"
instead.
* The "op " syntax for infix operators has been replaced by
"()". If 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 "\" 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>\argument\. 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. "\ \ARGUMENT\" or "\<^emph>\ARGUMENT\".
* 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 \ 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: \ \\\
- canceled source: \<^cancel>\\\
- raw LaTeX: \<^latex>\\\
* 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 \prop\ 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 \ A . f Y \ 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\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 "\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: \ \text\ (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 \* 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 \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10)
"_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PI _:_./ _)" 10)
"_lam" :: "pttrn \ 'a set \ 'a \ 'b \*