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