--- 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%
%