diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Aug 31 22:55:49 2006 +0200
@@ -5,45 +5,42 @@
 
 chapter {* Primitive logic *}
 
-section {* Syntax *}
+section {* Variable names *}
 
-subsection {* Variable names *}
+text FIXME
+
+
+section {* Types \label{sec:types} *}
 
 text {*
-  FIXME
+  \glossary{Type class}{FIXME}
+
+  \glossary{Type arity}{FIXME}
+
+  \glossary{Sort}{FIXME}
+
+  FIXME classes and sorts
+
+
+  \glossary{Type}{FIXME}
+
+  \glossary{Type constructor}{FIXME}
+
+  \glossary{Type variable}{FIXME}
+
+  FIXME simple types
 *}
 
 
-subsection {* Simply-typed lambda calculus *}
-
-text {*
-
-FIXME
-
-\glossary{Type}{FIXME}
-\glossary{Term}{FIXME}
-
-*}
-
-subsection {* The order-sorted algebra of types *}
+section {* Terms \label{sec:terms} *}
 
 text {*
-
-FIXME
-
-\glossary{Type constructor}{FIXME}
+  \glossary{Term}{FIXME}
 
-\glossary{Type class}{FIXME}
-
-\glossary{Type arity}{FIXME}
-
-\glossary{Sort}{FIXME}
-
+  FIXME de-Bruijn representation of lambda terms
 *}
 
 
-subsection {* Type-inference and schematic polymorphism *}
-
 text {*
 
 FIXME
@@ -55,21 +52,7 @@
 *}
 
 
-section {* Theory *}
-
-text {*
-
-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.}}
-
-*}
-
-
-section {* Deduction *}
+section {* Theorems \label{sec:thms} *}
 
 text {*
 
@@ -139,8 +122,21 @@
 text FIXME
 
 
-section {* Proof terms *}
+section {* Low-level specifications *}
+
+text {*
+
+FIXME
 
-text 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