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