diff -r 9dbb01456031 -r 0fb7891f0c7c doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Sun Oct 24 03:43:12 2010 -0700
+++ b/doc-src/IsarImplementation/implementation.tex	Sun Oct 24 15:11:24 2010 -0700
@@ -4,6 +4,7 @@
 \usepackage{../iman,../extra,../isar,../proof}
 \usepackage[nohyphen,strings]{../underscore}
 \usepackage{../isabelle,../isabellesym}
+\usepackage{../ttbox,../rail,../railsetup}
 \usepackage{style}
 \usepackage{../pdfsetup}
 
@@ -22,6 +23,11 @@
 
 \makeindex
 
+\railterm{lbrace,rbrace,atsign}
+\railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym}
+\railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym}
+\railalias{dots}{\isasymdots}\railterm{dots}
+
 
 \begin{document}
 
@@ -76,18 +82,18 @@
 \listoffigures
 \clearfirst
 
+\setcounter{chapter}{-1}
+
+\input{Thy/document/ML.tex}
 \input{Thy/document/Prelim.tex}
 \input{Thy/document/Logic.tex}
+\input{Thy/document/Syntax.tex}
 \input{Thy/document/Tactic.tex}
 \input{Thy/document/Proof.tex}
-\input{Thy/document/Syntax.tex}
 \input{Thy/document/Isar.tex}
 \input{Thy/document/Local_Theory.tex}
 \input{Thy/document/Integration.tex}
 
-\appendix
-\input{Thy/document/ML.tex}
-
 \begingroup
 \tocentry{\bibname}
 \bibliographystyle{abbrv} \small\raggedright\frenchspacing