proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;
authorwenzelm
Mon, 08 Jun 2020 22:31:36 +0200
changeset 71928 ae643fb4ca30
parent 71927 ebcae4a19e78
child 71929 73ff22f99d38
proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy;
lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Mon Jun 08 21:56:06 2020 +0200
+++ b/lib/texinputs/isabellesym.sty	Mon Jun 08 22:31:36 2020 +0200
@@ -397,6 +397,7 @@
 \newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
 \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
 \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
+\newcommand{\isactrloracleUNDERSCOREname}{\isakeywordcontrol{oracle{\isacharunderscore}name}}
 \newcommand{\isactrlpath}{\isakeywordcontrol{path}}
 \newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
 \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}