doc-src/TutorialI/isabelle.sty

 %% License: GPL (GNU GENERAL PUBLIC LICENSE)
 %%
 %% macros for Isabelle generated LaTeX output
 %%
 
-%%% Simple document preparation (based on theory token language)
+%%% Simple document preparation (based on theory token language and symbols)
 
 % isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
 
 \newcommand{\isastyle}{\small\tt\slshape}
 \newcommand{\isastyleminor}{\small\tt\slshape}
 \newcommand{\isastyletext}{\normalsize\rm}
 \newcommand{\isastyletxt}{\rm}