--- a/NEWS Sat Jan 09 12:35:07 2016 +0100
+++ b/NEWS Sat Jan 09 12:58:57 2016 +0100
@@ -17,6 +17,16 @@
* Support for more arrow symbols, with rendering in LaTeX and
Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
+* Special notation \<struct> for the first implicit 'structure' in the
+context has been discontinued. Rare INCOMPATIBILITY, use explicit
+structure name instead, notably in indexed notation with block-subscript
+(e.g. \<odot>\<^bsub>A\<^esub>).
+
+* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
+counterpart \<box> as quantifier-like symbol. A small diamond is available as
+\<diamondop>; the old symbol \<struct> loses this rendering and any special
+meaning.
+
* Syntax for formal comments "-- text" now also supports the symbolic
form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
to update old sources.
@@ -342,10 +352,6 @@
* Keyword 'rewrites' identifies rewrite morphisms in interpretation
commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
-* Special notation \<struct> for the first implicit 'structure' in the context
-has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
-instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
-
* More gentle suppression of syntax along locale morphisms while
printing terms. Previously 'abbreviation' and 'notation' declarations
would be suppressed for morphisms except term identity. Now
--- a/etc/symbols Sat Jan 09 12:35:07 2016 +0100
+++ b/etc/symbols Sat Jan 09 12:58:57 2016 +0100
@@ -222,6 +222,7 @@
\<not> code: 0x0000ac group: logic abbrev: ~
\<box> code: 0x0025a1 group: logic
\<diamond> code: 0x0025c7 group: logic
+\<diamondop> code: 0x0022c4 group: operator
\<turnstile> code: 0x0022a2 group: relation abbrev: |-
\<Turnstile> code: 0x0022a8 group: relation abbrev: |=
\<tturnstile> code: 0x0022a9 group: relation abbrev: |-
@@ -346,7 +347,6 @@
\<lozenge> code: 0x0025ca
\<wp> code: 0x002118
\<wrong> code: 0x002240 group: relation
-\<struct> code: 0x0022c4
\<acute> code: 0x0000b4
\<index> code: 0x000131
\<dieresis> code: 0x0000a8
--- a/lib/texinputs/isabellesym.sty Sat Jan 09 12:35:07 2016 +0100
+++ b/lib/texinputs/isabellesym.sty Sat Jan 09 12:58:57 2016 +0100
@@ -220,16 +220,17 @@
\newcommand{\isasymOr}{\isamath{\bigvee}}
\newcommand{\isasymforall}{\isamath{\forall\,}}
\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
-\newcommand{\isasymnot}{\isamath{\neg}}
\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
+\newcommand{\isasymdiamondop}{\isamath{\diamond}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
\newcommand{\isasymturnstile}{\isamath{\vdash}}
\newcommand{\isasymTurnstile}{\isamath{\models}}
\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
\newcommand{\isasymstileturn}{\isamath{\dashv}}
-\newcommand{\isasymsurd}{\isamath{\surd}}
\newcommand{\isasymle}{\isamath{\le}}
\newcommand{\isasymge}{\isamath{\ge}}
\newcommand{\isasymlless}{\isamath{\ll}}
@@ -350,7 +351,6 @@
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymwrong}{\isamath{\wr}}
-\newcommand{\isasymstruct}{\isamath{\diamond}}
\newcommand{\isasymacute}{\isatext{\'\relax}}
\newcommand{\isasymindex}{\isatext{\i}}
\newcommand{\isasymdieresis}{\isatext{\"\relax}}