# HG changeset patch
# User wenzelm
# Date 1452340737 -3600
# Node ID 0046bacc5f5b02139b0e2d5feaf372b4ad6aab91
# Parent  f74a33b14200ece4de283066533a8fe8bd71f722
\<struct> loses its rendering and is superseded by \<diamondop>;
tuned;

diff -r f74a33b14200 -r 0046bacc5f5b NEWS
--- 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
diff -r f74a33b14200 -r 0046bacc5f5b etc/symbols
--- 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
diff -r f74a33b14200 -r 0046bacc5f5b lib/texinputs/isabellesym.sty
--- 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}}