NEWS

 
 
 *** 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
 action "isabelle.update-state" (shortcut S+ENTER) triggers manual
 update.

 situations. The text overview column takes over the role to indicate
 unfinished edits in the PIDE pipeline. This avoids flashing text display
 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
 implicit: a popup will show up unconditionally.
 
 * Additional abbreviations for syntactic completion may be specified in
 $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.
 

 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
 
 * 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.
 
 * Antiquotations @{command}, @{method}, @{attribute} print checked

 
 * (Co)datatype package:
   - 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').
 
 * Transfer: new methods for interactive debugging of 'transfer' and

       mset_le_def ~> subseteq_mset_def
       mset_less_def ~> subset_mset_def
       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.
 
 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the

 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
 
 * HOL-Statespace: command 'statespace' uses mandatory qualifier for
 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
 Theorem of Algebra. Ported from HOL Light.

 [approximation] for inequalities of transcendental functions. Uses
 hardware floating point arithmetic to randomly discover potential
 counterexamples. Counterexamples are certified with the "approximation"
 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)
   - added congruence rules to rewrite measure spaces under the sets