diff -r 419116f1157a -r e23770bc97c8 doc-src/IsarImplementation/Thy/isar.thy
--- a/doc-src/IsarImplementation/Thy/isar.thy	Thu Feb 26 08:44:44 2009 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-
-(* $Id$ *)
-
-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