\<struct> loses its rendering and is superseded by \<diamondop>;
authorwenzelm
Sat Jan 09 12:58:57 2016 +0100 (2016-01-09)
changeset 621080046bacc5f5b
parent 62107 f74a33b14200
child 62109 d65f80949ff1
\<struct> loses its rendering and is superseded by \<diamondop>;
tuned;
NEWS
etc/symbols
lib/texinputs/isabellesym.sty
     1.1 --- a/NEWS	Sat Jan 09 12:35:07 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 12:58:57 2016 +0100
     1.3 @@ -17,6 +17,16 @@
     1.4  * Support for more arrow symbols, with rendering in LaTeX and
     1.5  Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
     1.6  
     1.7 +* Special notation \<struct> for the first implicit 'structure' in the
     1.8 +context has been discontinued. Rare INCOMPATIBILITY, use explicit
     1.9 +structure name instead, notably in indexed notation with block-subscript
    1.10 +(e.g. \<odot>\<^bsub>A\<^esub>).
    1.11 +
    1.12 +* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
    1.13 +counterpart \<box> as quantifier-like symbol. A small diamond is available as
    1.14 +\<diamondop>; the old symbol \<struct> loses this rendering and any special
    1.15 +meaning.
    1.16 +
    1.17  * Syntax for formal comments "-- text" now also supports the symbolic
    1.18  form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
    1.19  to update old sources.
    1.20 @@ -342,10 +352,6 @@
    1.21  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
    1.22  commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
    1.23  
    1.24 -* Special notation \<struct> for the first implicit 'structure' in the context
    1.25 -has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
    1.26 -instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
    1.27 -
    1.28  * More gentle suppression of syntax along locale morphisms while
    1.29  printing terms. Previously 'abbreviation' and 'notation' declarations
    1.30  would be suppressed for morphisms except term identity. Now
     2.1 --- a/etc/symbols	Sat Jan 09 12:35:07 2016 +0100
     2.2 +++ b/etc/symbols	Sat Jan 09 12:58:57 2016 +0100
     2.3 @@ -222,6 +222,7 @@
     2.4  \<not>                  code: 0x0000ac  group: logic  abbrev: ~
     2.5  \<box>                  code: 0x0025a1  group: logic
     2.6  \<diamond>              code: 0x0025c7  group: logic
     2.7 +\<diamondop>            code: 0x0022c4  group: operator
     2.8  \<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
     2.9  \<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
    2.10  \<tturnstile>           code: 0x0022a9  group: relation  abbrev: |-
    2.11 @@ -346,7 +347,6 @@
    2.12  \<lozenge>              code: 0x0025ca
    2.13  \<wp>                   code: 0x002118
    2.14  \<wrong>                code: 0x002240  group: relation
    2.15 -\<struct>               code: 0x0022c4
    2.16  \<acute>                code: 0x0000b4
    2.17  \<index>                code: 0x000131
    2.18  \<dieresis>             code: 0x0000a8
     3.1 --- a/lib/texinputs/isabellesym.sty	Sat Jan 09 12:35:07 2016 +0100
     3.2 +++ b/lib/texinputs/isabellesym.sty	Sat Jan 09 12:58:57 2016 +0100
     3.3 @@ -220,16 +220,17 @@
     3.4  \newcommand{\isasymOr}{\isamath{\bigvee}}
     3.5  \newcommand{\isasymforall}{\isamath{\forall\,}}
     3.6  \newcommand{\isasymexists}{\isamath{\exists\,}}
     3.7 +\newcommand{\isasymnot}{\isamath{\neg}}
     3.8  \newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
     3.9 -\newcommand{\isasymnot}{\isamath{\neg}}
    3.10  \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
    3.11  \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
    3.12 +\newcommand{\isasymdiamondop}{\isamath{\diamond}}
    3.13 +\newcommand{\isasymsurd}{\isamath{\surd}}
    3.14  \newcommand{\isasymturnstile}{\isamath{\vdash}}
    3.15  \newcommand{\isasymTurnstile}{\isamath{\models}}
    3.16  \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
    3.17  \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
    3.18  \newcommand{\isasymstileturn}{\isamath{\dashv}}
    3.19 -\newcommand{\isasymsurd}{\isamath{\surd}}
    3.20  \newcommand{\isasymle}{\isamath{\le}}
    3.21  \newcommand{\isasymge}{\isamath{\ge}}
    3.22  \newcommand{\isasymlless}{\isamath{\ll}}
    3.23 @@ -350,7 +351,6 @@
    3.24  \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
    3.25  \newcommand{\isasymwp}{\isamath{\wp}}
    3.26  \newcommand{\isasymwrong}{\isamath{\wr}}
    3.27 -\newcommand{\isasymstruct}{\isamath{\diamond}}
    3.28  \newcommand{\isasymacute}{\isatext{\'\relax}}
    3.29  \newcommand{\isasymindex}{\isatext{\i}}
    3.30  \newcommand{\isasymdieresis}{\isatext{\"\relax}}