1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarImplementation/Thy/isar.thy	Mon Sep 04 17:06:45 2006 +0200
     1.3 @@ -0,0 +1,36 @@
     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 states \label{sec:isar-proof-state} *}
    1.12 +
    1.13 +text {*
    1.14 +  FIXME
    1.15 +
    1.16 +\glossary{Proof state}{The whole configuration of a structured proof,
    1.17 +consisting of a \seeglossary{proof context} and an optional
    1.18 +\seeglossary{structured goal}.  Internally, an Isar proof state is
    1.19 +organized as a stack to accomodate block structure of proof texts.
    1.20 +For historical reasons, a low-level \seeglossary{tactical goal} is
    1.21 +occasionally called ``proof state'' as well.}
    1.22 +
    1.23 +\glossary{Structured goal}{FIXME}
    1.24 +
    1.25 +\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
    1.26 +
    1.27 +
    1.28 +*}
    1.29 +
    1.30 +section {* Proof methods *}
    1.31 +
    1.32 +text FIXME
    1.33 +
    1.34 +section {* Attributes *}
    1.35 +
    1.36 +text "FIXME ?!"
    1.37 +
    1.38 +
    1.39 +end