1.1 --- a/doc-src/IsarImplementation/Thy/isar.thy Wed Mar 04 11:05:02 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,41 +0,0 @@
1.4 -
1.5 -(* $Id$ *)
1.6 -
1.7 -theory isar imports base begin
1.8 -
1.9 -chapter {* Isar proof texts *}
1.10 -
1.11 -section {* Proof context *}
1.12 -
1.13 -text FIXME
1.14 -
1.15 -
1.16 -section {* Proof state \label{sec:isar-proof-state} *}
1.17 -
1.18 -text {*
1.19 - FIXME
1.20 -
1.21 -\glossary{Proof state}{The whole configuration of a structured proof,
1.22 -consisting of a \seeglossary{proof context} and an optional
1.23 -\seeglossary{structured goal}. Internally, an Isar proof state is
1.24 -organized as a stack to accomodate block structure of proof texts.
1.25 -For historical reasons, a low-level \seeglossary{tactical goal} is
1.26 -occasionally called ``proof state'' as well.}
1.27 -
1.28 -\glossary{Structured goal}{FIXME}
1.29 -
1.30 -\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
1.31 -
1.32 -
1.33 -*}
1.34 -
1.35 -section {* Proof methods *}
1.36 -
1.37 -text FIXME
1.38 -
1.39 -section {* Attributes *}
1.40 -
1.41 -text "FIXME ?!"
1.42 -
1.43 -
1.44 -end