# HG changeset patch # User wenzelm # Date 1686130824 -7200 # Node ID a502d7e0685502a95bd868fe7bc0fda78d548e0d # Parent 4565761532496691ced8eeca7b07ea5ffcd91881 tuned NEWS; diff -r 456576153249 -r a502d7e06855 NEWS --- a/NEWS Tue Jun 06 23:42:47 2023 +0200 +++ b/NEWS Wed Jun 07 11:40:24 2023 +0200 @@ -28,6 +28,9 @@ *** Document preparation *** +* Support for interactive document preparation in PIDE, notably via the +Isabelle/jEdit Document panel. + * Various well-known LaTeX styles are included as Isabelle components, with demo documents in the regular Isabelle "doc" space: @@ -37,9 +40,6 @@ - Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics" - Springer LaTeX LNCS style as session "Demo_LLNCS" / doc "demo_llncs" -* Support for interactive document preparation in PIDE, notably via the -Isabelle/jEdit Document panel. - * Support for more "cite" antiquotations, notably for \nocite and natbib's \citet / \citep. The antiquotation syntax now supports control-symbol-cartouche form, with an embedded argument: @@ -62,15 +62,22 @@ *** HOL *** -* Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings"; - "euclidean division" typically denotes a particular division on - integers. Minor INCOMPATIBILITY. - -* Theory "HOL.Fun": - - Renamed lemma inj_on_strict_subset to image_strict_mono. +* Sledgehammer: + - Added an inconsistency check mode to find likely unprovable + conjectures. It is enabled by default in addition to the usual + proving mode and can be controlled using the 'falsify' option. + - Added an abduction mode to find likely missing hypotheses to + conjectures. It currently works only with the E prover. It is + enabled by default and can be controlled using the 'abduce' option. + +* Metis: + - Made clausifier more robust in the face of nested lambdas. Minor INCOMPATIBILITY. -* Theory HOL.Map: +* 'primcorec': Made the internal tactic more robust in the face of + nested corecursion. + +* Theory "HOL.Map": - Map.empty has been demoted to an input abbreviation. - Map update syntax "_(_ \ _)" now has the same priorities as function update syntax "_(_ := _)". This means: @@ -82,6 +89,14 @@ Except in "[...]" maps where ":=" would create a clash with list update syntax "xs[i := x]". +* Theory "HOL.Fun": + - Renamed lemma inj_on_strict_subset to image_strict_mono. + Minor INCOMPATIBILITY. + +* Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings"; + "euclidean division" typically denotes a particular division on + integers. Minor INCOMPATIBILITY. + * Theory "HOL.Finite_Set" - Imported Relation instead of Product_Type, Sum_Type, and Fields. Minor INCOMPATIBILITY. @@ -102,22 +117,22 @@ irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are explicitly provided for backward compatibility but their usage is discouraged. Minor INCOMPATIBILITY. - - Added predicates sym_on and symp_on and redefined sym and - symp to be abbreviations. Lemmas sym_def and symp_def are explicitly - provided for backward compatibility but their usage is discouraged. - Minor INCOMPATIBILITY. - - Added predicates asym_on and asymp_on and redefined asym and - asymp to be abbreviations. INCOMPATIBILITY. - - Added predicates antisym_on and antisymp_on and redefined antisym and - antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are + - Added predicates sym_on and symp_on and redefined sym and symp to be + abbreviations. Lemmas sym_def and symp_def are explicitly provided + for backward compatibility but their usage is discouraged. Minor + INCOMPATIBILITY. + - Added predicates asym_on and asymp_on and redefined asym and asymp + to be abbreviations. INCOMPATIBILITY. + - Added predicates antisym_on and antisymp_on and redefined antisym + and antisymp to be abbreviations. Lemmas antisym_def and + antisymp_def are explicitly provided for backward compatibility but + their usage is discouraged. Minor INCOMPATIBILITY. + - Added predicates trans_on and transp_on and redefined trans and + transp to be abbreviations. Lemmas trans_def and transp_def are explicitly provided for backward compatibility but their usage is discouraged. Minor INCOMPATIBILITY. - - Added predicates trans_on and transp_on and redefined trans and transp to - be abbreviations. Lemmas trans_def and transp_def are explicitly provided - for backward compatibility but their usage is discouraged. - Minor INCOMPATIBILITY. - - Renamed wrongly named lemma totalp_on_refl_on_eq to totalp_on_total_on_eq. - Minor INCOMPATIBILITY. + - Renamed wrongly named lemma totalp_on_refl_on_eq to + totalp_on_total_on_eq. Minor INCOMPATIBILITY. - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY. antisym_converse[simp] ~> antisym_on_converse[simp] order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp] @@ -241,8 +256,8 @@ fimage_strict_mono wfP_pfsubset -* Theory "HOL-Library.BigO": - - Obsolete, moved to HOL-ex +* Theory "HOL-Library.BigO" is obsolete and has been moved to + "HOL-ex.BigO" (it corresponds to "HOL-Metis_Examples.Big_O"). * Theory "HOL-Library.Multiset": - Strengthened lemmas. Minor INCOMPATIBILITIES. @@ -255,8 +270,8 @@ multp_cancel_add_mset multp_cancel_max multp_code_iff_mult - - Used transp_on and reorder assumptions of lemmas bex_least_element and - bex_greatest_element. Minor INCOMPATIBILITIES. + - Used transp_on and reorder assumptions of lemmas bex_least_element + and bex_greatest_element. Minor INCOMPATIBILITIES. - Added lemmas. count_minus_inter_lt_count_minus_inter_iff minus_inter_eq_minus_inter_iff @@ -296,34 +311,18 @@ transp_multpHO transp_on_multpHO -* 'primcorec': Made the internal tactic more robust in the face of - nested corecursion. - -* HOL-Algebra: new theories SimpleGroups (simple groups) - and SndIsomorphismGrp (second isomorphism theorem for groups), - by Jakob von Raumer - -* HOL-Analysis: - - imported the HOL Light abstract metric space library and - numerous associated topological developments - - new material on infinite sums and integration, due to Manuel Eberl +* Session "HOL-Algebra": new theories "HOL-Algebra.SimpleGroups" and +"HOL-Algebra.SndIsomorphismGrp" (second isomorphism theorem for groups), +by Jakob von Raumer. + +* Session "HOL-Analysis": + - Imported the HOL Light abstract metric space library and numerous + associated topological developments. + - New material on infinite sums and integration, due to Manuel Eberl and Wenda Li. -* Mirabelle: - - Added session to output directory structure. Minor INCOMPATIBILITY. - -* Metis: - - Made clausifier more robust in the face of nested lambdas. - Minor INCOMPATIBILITY. - -* Sledgehammer: - - Added an inconsistency check mode to find likely unprovable - conjectures. It is enabled by default in addition to the usual - proving mode and can be controlled using the 'falsify' option. - - Added an abduction mode to find likely missing hypotheses to - conjectures. It currently works only with the E prover. It is - enabled by default and can be controlled using the 'abduce' - option. +* Session "Mirabelle": Added session name to output directory structure. +Minor INCOMPATIBILITY. *** ML *** @@ -425,10 +424,6 @@ "process_policy", as it may affect other processes as well (notably in "isabelle build"). -* Isabelle/Scala provides generic support for XZ and Zstd compression, -via Compress.Options and Compress.Cache. Bytes.uncompress automatically -detects the compression scheme. - * The command-line tools "isabelle dotnet_setup" and "isabelle dotnet" support the Dotnet platform (.NET), which includes Fsharp (F#). This works uniformly on all Isabelle OS platforms, even as cross-platform @@ -451,6 +446,10 @@ the property {"verbose": bool} indicates whether the result is meant to depend on verbose mode. +* Isabelle/Scala provides generic support for XZ and Zstd compression, +via Compress.Options and Compress.Cache. Bytes.uncompress automatically +detects the compression scheme. + New in Isabelle2022 (October 2022)