# HG changeset patch
# User wenzelm
# Date 1234815814 -3600
# Node ID bcb79ddf57da2da0de9ca375eefbd7c275b4f27d
# Parent  7a3b5bbed31318e586506177495374f3889af715
removed rudiments of glossary;
tuned outline;

diff -r 7a3b5bbed313 -r bcb79ddf57da doc-src/IsarImplementation/Thy/Isar.thy
--- a/doc-src/IsarImplementation/Thy/Isar.thy	Mon Feb 16 21:23:33 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Mon Feb 16 21:23:34 2009 +0100
@@ -2,39 +2,36 @@
 imports Base
 begin
 
-chapter {* Isar proof texts *}
+chapter {* Isar language elements *}
+
+text {*
+  The primary Isar language consists of three main categories of
+  language elements:
+
+  \begin{enumerate}
+
+  \item Proof commands
 
-section {* Proof context *}
+  \item Proof methods
+
+  \item Attributes
+
+  \end{enumerate}
+*}
+
+
+section {* Proof commands *}
 
 text FIXME
 
 
-section {* Proof state \label{sec:isar-proof-state} *}
-
-text {*
-  FIXME
-
-\glossary{Proof state}{The whole configuration of a structured proof,
-consisting of a \seeglossary{proof context} and an optional
-\seeglossary{structured goal}.  Internally, an Isar proof state is
-organized as a stack to accomodate block structure of proof texts.
-For historical reasons, a low-level \seeglossary{tactical goal} is
-occasionally called ``proof state'' as well.}
-
-\glossary{Structured goal}{FIXME}
-
-\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
-
-
-*}
-
 section {* Proof methods *}
 
 text FIXME
 
+
 section {* Attributes *}
 
-text "FIXME ?!"
-
+text FIXME
 
 end
diff -r 7a3b5bbed313 -r bcb79ddf57da doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Mon Feb 16 21:23:33 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Mon Feb 16 21:23:34 2009 +0100
@@ -2,24 +2,17 @@
 imports Base
 begin
 
-chapter {* Structured specifications *}
+chapter {* Local theory specifications *}
+
+section {* Definitional elements *}
 
-section {* Specification elements *}
-
-text FIXME
+text {*
+  FIXME
+*}
 
 
-section {* Type-inference *}
+section {* Morphisms and declarations *}
 
 text FIXME
 
-
-section {* Local theories *}
-
-text {*
-  FIXME
-
-  \glossary{Local theory}{FIXME}
-*}
-
 end