# HG changeset patch # User wenzelm # Date 1635091378 -7200 # Node ID 7f311d474cf945c75b91124a757a034017dc5a29 # Parent 40910c47d7a1ce1ead91c6158e5e024b67b528a7 more control symbols; diff -r 40910c47d7a1 -r 7f311d474cf9 etc/symbols --- a/etc/symbols Sun Oct 24 16:43:54 2021 +0200 +++ b/etc/symbols Sun Oct 24 18:02:58 2021 +0200 @@ -456,6 +456,7 @@ \<^cterm> argument: cartouche \<^ctyp> argument: cartouche \<^keyword> argument: cartouche +\<^let> argument: cartouche \<^locale> argument: cartouche \<^make_judgment> \<^dest_judgment> @@ -505,4 +506,3 @@ \<^if_macos> argument: cartouche \<^if_windows> argument: cartouche \<^if_unix> argument: cartouche - diff -r 40910c47d7a1 -r 7f311d474cf9 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Sun Oct 24 16:43:54 2021 +0200 +++ b/lib/texinputs/isabellesym.sty Sun Oct 24 18:02:58 2021 +0200 @@ -446,6 +446,7 @@ \newcommand{\isactrlhere}{\isakeywordcontrol{here}} \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} \newcommand{\isactrllatex}{\isakeywordcontrol{latex}} +\newcommand{\isactrllet}{\isakeywordcontrol{let}} \newcommand{\isactrllocale}{\isakeywordcontrol{locale}} \newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}} \newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}