--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Mon Feb 16 20:47:44 2009 +0100
@@ -0,0 +1,40 @@
+theory Isar
+imports Base
+begin
+
+chapter {* Isar proof texts *}
+
+section {* Proof context *}
+
+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 ?!"
+
+
+end