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