--- a/doc-src/IsarImplementation/implementation.tex Tue May 08 15:01:33 2007 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Tue May 08 15:36:39 2007 +0200
@@ -66,7 +66,7 @@
\listoffigures
\clearfirst
-\input{intro.tex}
+%\input{intro.tex}
\input{Thy/document/prelim.tex}
\input{Thy/document/logic.tex}
\input{Thy/document/tactic.tex}
--- a/doc-src/IsarImplementation/style.sty Tue May 08 15:01:33 2007 +0200
+++ b/doc-src/IsarImplementation/style.sty Tue May 08 15:36:39 2007 +0200
@@ -45,6 +45,10 @@
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
\renewcommand{\endisatagmlref}{\endgroup}
+\newcommand{\minorcmd}[1]{{\sf #1}}
+\newcommand{\isasymtype}{\minorcmd{type}}
+\newcommand{\isasymval}{\minorcmd{val}}
+
\newcommand{\isasymGUESS}{\isakeyword{guess}}
\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
\newcommand{\isasymTHEORY}{\isakeyword{theory}}