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