# HG changeset patch
# User wenzelm
# Date 1178631399 -7200
# Node ID c82dd66560acc036d0e13f862fe2737811dfd490
# Parent  165f733c50bd9fb47e1a1fe6069e591801a7d4bd
tuned;

diff -r 165f733c50bd -r c82dd66560ac doc-src/IsarImplementation/implementation.tex
--- 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}
diff -r 165f733c50bd -r c82dd66560ac doc-src/IsarImplementation/style.sty
--- 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}}