latex macro for \<^const>;
authorwenzelm
Sat Jan 05 17:00:43 2019 +0100 (6 months ago)
changeset 69596c8a2755bf220
parent 69595 ec135235fbcc
child 69597 ff784d5a5bfb
latex macro for \<^const>;
lib/texinputs/isabellesym.sty
     1.1 --- a/lib/texinputs/isabellesym.sty	Sat Jan 05 15:15:21 2019 +0100
     1.2 +++ b/lib/texinputs/isabellesym.sty	Sat Jan 05 17:00:43 2019 +0100
     1.3 @@ -373,6 +373,7 @@
     1.4  \newcommand{\isactrlclass}{\isakeywordcontrol{class}}
     1.5  \newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
     1.6  \newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
     1.7 +\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
     1.8  \newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
     1.9  \newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
    1.10  \newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}