diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu Aug 31 22:55:49 2006 +0200
@@ -23,11 +23,7 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Syntax%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Variable names%
+\isamarkupsection{Variable names%
 }
 \isamarkuptrue%
 %
@@ -36,39 +32,41 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Simply-typed lambda calculus%
+\isamarkupsection{Types \label{sec:types}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME
+\glossary{Type class}{FIXME}
+
+  \glossary{Type arity}{FIXME}
+
+  \glossary{Sort}{FIXME}
+
+  FIXME classes and sorts
 
-\glossary{Type}{FIXME}
-\glossary{Term}{FIXME}%
+
+  \glossary{Type}{FIXME}
+
+  \glossary{Type constructor}{FIXME}
+
+  \glossary{Type variable}{FIXME}
+
+  FIXME simple types%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{The order-sorted algebra of types%
+\isamarkupsection{Terms \label{sec:terms}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME
-
-\glossary{Type constructor}{FIXME}
-
-\glossary{Type class}{FIXME}
+\glossary{Term}{FIXME}
 
-\glossary{Type arity}{FIXME}
-
-\glossary{Sort}{FIXME}%
+  FIXME de-Bruijn representation of lambda terms%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Type-inference and schematic polymorphism%
-}
-\isamarkuptrue%
-%
 \begin{isamarkuptext}%
 FIXME
 
@@ -78,21 +76,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Theory%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
-theory context, but slightly more flexible since it may be used at
-different type-instances, due to \seeglossary{schematic
-polymorphism.}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Deduction%
+\isamarkupsection{Theorems \label{sec:thms}%
 }
 \isamarkuptrue%
 %
@@ -171,12 +155,21 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Proof terms%
+\isamarkupsection{Low-level specifications%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+FIXME
+
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}
+
+\glossary{Axiom}{FIXME}
+
+\glossary{Primitive definition}{FIXME}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %