# HG changeset patch # User wenzelm # Date 1452340737 -3600 # Node ID 0046bacc5f5b02139b0e2d5feaf372b4ad6aab91 # Parent f74a33b14200ece4de283066533a8fe8bd71f722 \ loses its rendering and is superseded by \; 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: \ \ \ \ \ \ +* Special notation \ 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. \\<^bsub>A\<^esub>). + +* The glyph for \ in the IsabelleText font now corresponds better to its +counterpart \ as quantifier-like symbol. A small diamond is available as +\; the old symbol \ loses this rendering and any special +meaning. + * Syntax for formal comments "-- text" now also supports the symbolic form "\ 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 \ 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. \\<^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 @@ \ code: 0x0000ac group: logic abbrev: ~ \ code: 0x0025a1 group: logic \ code: 0x0025c7 group: logic +\ code: 0x0022c4 group: operator \ code: 0x0022a2 group: relation abbrev: |- \ code: 0x0022a8 group: relation abbrev: |= \ code: 0x0022a9 group: relation abbrev: |- @@ -346,7 +347,6 @@ \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 group: relation -\ code: 0x0022c4 \ code: 0x0000b4 \ code: 0x000131 \ 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}}