doc-src/IsarImplementation/Thy/logic.thy
changeset 20477 e623b0e30541
parent 20472 e993073eda4c
child 20480 4e0522d38968
--- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:23 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 16:42:32 2006 +0200
@@ -5,11 +5,6 @@
 
 chapter {* Primitive logic \label{ch:logic} *}
 
-section {* Names *}
-
-text FIXME
-
-
 section {* Types \label{sec:types} *}
 
 text {*
@@ -52,6 +47,13 @@
 *}
 
 
+section {* Proof terms *}
+
+text {*
+  FIXME
+*}
+
+
 section {* Theorems \label{sec:thms} *}
 
 text {*
@@ -122,7 +124,7 @@
 text FIXME
 
 
-section {* Low-level specifications *}
+section {* Raw theories *}
 
 text {*