NEWS
changeset 62234 7cc9d7b822ae
parent 62231 25f4a9cd8b68
child 62235 3687c199e22b
--- a/NEWS	Sat Jan 23 23:50:54 2016 +0100
+++ b/NEWS	Sun Jan 24 12:21:57 2016 +0100
@@ -101,6 +101,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.