--- a/NEWS Sat Oct 02 20:00:02 2021 +0200
+++ b/NEWS Sat Oct 02 20:27:13 2021 +0200
@@ -4,16 +4,16 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
-New in this Isabelle version
-----------------------------
+New in Isabelle2021 (December 2021)
+-----------------------------------
*** General ***
* Commands 'syntax' and 'no_syntax' now work in a local theory context,
-but there is no proper way to refer to local entities --- in contrast to
-'notation' and 'no_notation'. Local syntax works well with 'bundle',
-e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
-Isabelle/HOL.
+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.
* Configuration option "show_results" controls output of final results
in commands like 'definition' or 'theorem'. Output is normally enabled
@@ -26,19 +26,6 @@
theorem test by (simp add: test_def)
end
-* Timeouts for Isabelle/ML tools are subject to system option
-"timeout_scale" --- this already used for the overall session build
-process before, and allows to adapt to slow machines. The underlying
-Timeout.apply in Isabelle/ML treats an original timeout specification 0
-as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
-in boundary cases.
-
-* 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
-
* More symbol definitions for the Z Notation (Isabelle fonts and LaTeX).
See also the group "Z Notation" in the Symbols dockable of
Isabelle/jEdit.
@@ -143,6 +130,63 @@
*** HOL ***
+* 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.
+
+* 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.
+
+* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
+
+* Simplified class hierarchy for bit operations: bit operations reside
+in classes (semi)ring_bit_operations, class semiring_bit_shifts is
+gone.
+
+* Expressions of the form "NOT (numeral _)" are not simplified by
+default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq
+as simp rule explicitly if needed.
+
+* 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.
+
+* Sledgehammer:
+ - 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.
+
* 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
@@ -181,20 +225,9 @@
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
+with the function "arg" of Complex_Main, renaming arg ~> Arg also in the
names of arg_bounded. Minor INCOMPATIBILITY.
-* 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.
-
* 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".
@@ -208,52 +241,6 @@
* Theory "HOL-Combinatorics.Transposition" provides elementary swap
operation "transpose".
-* 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.
-
-* 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.
-
-* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
-
-* Simplified class hierarchy for bit operations: bit operations reside
-in classes (semi)ring_bit_operations, class semiring_bit_shifts is
-gone.
-
-* Expressions of the form "NOT (numeral _)" are not simplified by
-default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq
-as simp rule explicitly if needed.
-
-* 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.
-
-* Sledgehammer:
- - 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.
-
*** ML ***
@@ -380,6 +367,17 @@
- Isabelle_System.rm_tree
- Isabelle_System.download
+* 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 ***
@@ -406,16 +404,18 @@
isabelle.jedit module is now part of Isabelle/Scala (as one big
$ISABELLE_SCALA_JAR).
-* 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.
+* Timeouts for Isabelle/ML tools are subject to system option
+"timeout_scale" --- this already used for the overall session build
+process before, and allows to adapt to slow machines. The underlying
+Timeout.apply in Isabelle/ML treats an original timeout specification 0
+as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
+in boundary cases.
+
+* 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 option "system_log" specifies an optional log file for internal
messages produced by Output.system_message in Isabelle/ML; the value
@@ -429,7 +429,7 @@
can be used in the short form. E.g. "isabelle build -o document".
* Command-line tool "isabelle version" supports repository archives
-(without full .hg directory). More options.
+(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