obsolete (used to be part of old src/Pure/codegen.ML);
authorwenzelm
Thu Dec 07 11:12:55 2017 +0100 (7 months ago)
changeset 6715339117b6f0b2e
parent 67152 8021ea06aad8
child 67154 c7def8f836d0
obsolete (used to be part of old src/Pure/codegen.ML);
lib/texinputs/isabellesym.sty
     1.1 --- a/lib/texinputs/isabellesym.sty	Wed Dec 06 21:43:20 2017 +0100
     1.2 +++ b/lib/texinputs/isabellesym.sty	Thu Dec 07 11:12:55 2017 +0100
     1.3 @@ -357,7 +357,6 @@
     1.4  \newcommand{\isasymdieresis}{\isatext{\"\relax}}
     1.5  \newcommand{\isasymcedilla}{\isatext{\c\relax}}
     1.6  \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
     1.7 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
     1.8  \newcommand{\isasymsome}{\isamath{\epsilon\,}}
     1.9  \newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
    1.10  \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}