# HG changeset patch # User wenzelm # Date 1591648296 -7200 # Node ID ae643fb4ca30ef17fb57ab98e892e1f897b2b72e # Parent ebcae4a19e785bf2dcc8a18a9123b6a03035f806 proper latex macros, notably for src/HOL/Examples/Iff_Oracle.thy; diff -r ebcae4a19e78 -r ae643fb4ca30 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}}