# 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}}