changeset 64525 | 9c3da2276e19 |
parent 63590 | 4854f7ee0987 |
child 67139 | 8fe0aba577af |
--- a/lib/texinputs/isabelle.sty Thu Nov 24 15:21:54 2016 +0100 +++ b/lib/texinputs/isabelle.sty Fri Nov 25 14:10:33 2016 +0100 @@ -73,7 +73,7 @@ \newcommand{\isadigit}[1]{#1} \newcommand{\isachardefaults}{% -\def\isacharbell{\isamath{\bigbox}} %requires stmaryrd +\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd \chardef\isacharbang=`\!% \chardef\isachardoublequote=`\"% \chardef\isachardoublequoteopen=`\"%