--- a/NEWS Wed Feb 10 15:49:05 2016 +0100
+++ b/NEWS Fri Feb 12 22:36:48 2016 +0100
@@ -66,13 +66,13 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the source-level debugger of Poly/ML, to work with
-Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
-and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
-'SML_file_no_debug' control compilation of sources with debugging
-information. The Debugger panel allows to set breakpoints (via context
-menu), step through stopped threads, evaluate local ML expressions etc.
-At least one Debugger view needs to be active to have any effect on the
-running ML program.
+Isabelle/ML and official Standard ML. Option "ML_debugger" and commands
+'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
+'SML_file_no_debug' control compilation of sources with or without
+debugging information. The Debugger panel allows to set breakpoints (via
+context menu), step through stopped threads, evaluate local ML
+expressions etc. At least one Debugger view needs to be active to have
+any effect on the running ML program.
* The State panel manages explicit proof state output, with dynamic
auto-update according to cursor movement. Alternatively, the jEdit
@@ -95,8 +95,8 @@
due to ad-hoc updates by auxiliary GUI components, such as the State
panel.
-* Improved scheduling for urgent print tasks (e.g. command state output,
-interactive queries) wrt. long-running background tasks.
+* Slightly improved scheduling for urgent print tasks (e.g. command
+state output, interactive queries) wrt. long-running background tasks.
* Completion of symbols via prefix of \<name> or \<^name> or \name is
always possible, independently of the language context. It is never
@@ -106,6 +106,11 @@
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
support for simple templates using ASCII 007 (bell) as placeholder.
+* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for
+completion like "+o", "*o", ".o" etc. -- due to conflicts with other
+ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
+suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
+
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
@@ -183,8 +188,8 @@
* Antiquotation @{verbatim [display]} supports option "indent".
* Antiquotation @{theory_text} prints uninterpreted theory source text
-(outer syntax with command keywords etc.). This may be used in the short
-form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
+(Isar outer syntax with command keywords etc.). This may be used in the
+short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
* Antiquotation @{doc ENTRY} provides a reference to the given
documentation, with a hyperlink in the Prover IDE.
@@ -594,8 +599,8 @@
- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
structure on the raw type to an abstract type defined using typedef.
- Always generate "case_transfer" theorem.
- - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct",
- and "coinduct" theorems. INCOMPATIBLITY.
+ - For mutual types, generate slightly stronger "rel_induct",
+ "rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY.
- Allow discriminators and selectors with the same name as the type
being defined.
- Avoid various internal name clashes (e.g., 'datatype f = f').
@@ -682,8 +687,8 @@
less_eq_multiset.rep_eq ~> subseteq_mset_def
INCOMPATIBILITY
- Removed lemmas generated by lift_definition:
- less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
- less_eq_multiset_def
+ less_eq_multiset.abs_eq, less_eq_multiset.rsp,
+ less_eq_multiset.transfer, less_eq_multiset_def
INCOMPATIBILITY
* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.
@@ -708,6 +713,9 @@
import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
remove '!' and add '?' as required.
+* HOL-Decision_Procs: The "approximation" method works with "powr"
+(exponentiation on real numbers) again.
+
* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
integrals (= complex path integrals), Cauchy's integral theorem, winding
numbers and Cauchy's integral formula, Liouville theorem, Fundamental
@@ -1249,9 +1257,6 @@
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
examples.
-* HOL-Decision_Procs: The "approximation" method works with "powr"
- (exponentiation on real numbers) again.
-
* HOL-Probability: Reworked measurability prover
- applies destructor rules repeatedly
- removed application splitting (replaced by destructor rule)