# HG changeset patch # User wenzelm # Date 1728077884 -7200 # Node ID 7b3b27576f45cbc3ac7e0d8bc1fd5fb4e9febdde # Parent 6538332c08e0694775198ffb2a46e6b6178cf4b1 misc tuning; diff -r 6538332c08e0 -r 7b3b27576f45 NEWS --- a/NEWS Fri Oct 04 15:21:01 2024 +0200 +++ b/NEWS Fri Oct 04 23:38:04 2024 +0200 @@ -36,16 +36,16 @@ *** Isabelle/VSCode Prover IDE *** * General improvements: Persistent decorations for PIDE markup, correct - font and formatting in panels, and proper completions. - Moreover, the PIDE extension of the LSP now features additional - protocol messages (e.g. to obtain the set of Isabelle symbols) and - more fine-grained control for unicode symbols. - -* Active "sendback" markup can now be used via LSP code actions, e.g. - to insert proof methods from Sledgehammer output. +font and formatting in panels, and proper completions. Moreover, the +PIDE extension of the LSP now features additional protocol messages +(e.g. to obtain the set of Isabelle symbols) and more fine-grained +control for recoding of Unicode symbols. + +* Active "sendback" markup can now be used via LSP code actions, e.g. to +insert proof methods from Sledgehammer output. * Relevant Isabelle options can now be overriden from the - Isabelle/VSCode extension settings. +Isabelle/VSCode extension settings. *** HOL *** @@ -65,7 +65,7 @@ * Theory "HOL.Wellfounded": - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead. - Minor INCOMPATIBILITIES. + Minor INCOMPATIBILITY. - Renamed lemmas. Minor INCOMPATIBILITY. accp_wfPD ~> accp_wfpD accp_wfPI ~> accp_wfpI @@ -99,13 +99,13 @@ image_mset_diff_if_inj minus_add_mset_if_not_in_lhs[simp] -* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and supposed to -be removed in a furure release. Minor INCOMPATIBILITY. Import -"HOL-Library.Divides" and keep an eye on theorems prefixed with "Divides." to -ease transition. +* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and +supposed to be removed in a furure release. Minor INCOMPATIBILITY. +Import "HOL-Library.Divides" and keep an eye on theorems prefixed with +"Divides." to ease transition. * The real-valued versions of ln, log, powr have been totalised by -ln(0) = x and ln(-x) = ln(x). Many related theorems are now +"ln(0) = x" and "ln(-x) = ln(x)". Many related theorems are now unconditional, with ln_mult_pos and ln_divide_pos introduced for legacy purposes.