doc-src/IsarImplementation/Thy/isar.thy
author wenzelm
Tue Sep 12 17:45:58 2006 +0200 (2006-09-12)
changeset 20520 05fd007bdeb9
parent 20472 e993073eda4c
permissions -rw-r--r--
tuned;
wenzelm@20472
     1
wenzelm@20472
     2
(* $Id$ *)
wenzelm@20472
     3
wenzelm@20472
     4
theory isar imports base begin
wenzelm@20472
     5
wenzelm@20472
     6
chapter {* Isar proof texts *}
wenzelm@20472
     7
wenzelm@20520
     8
section {* Proof context *}
wenzelm@20520
     9
wenzelm@20520
    10
text FIXME
wenzelm@20520
    11
wenzelm@20520
    12
wenzelm@20520
    13
section {* Proof state \label{sec:isar-proof-state} *}
wenzelm@20472
    14
wenzelm@20472
    15
text {*
wenzelm@20472
    16
  FIXME
wenzelm@20472
    17
wenzelm@20472
    18
\glossary{Proof state}{The whole configuration of a structured proof,
wenzelm@20472
    19
consisting of a \seeglossary{proof context} and an optional
wenzelm@20472
    20
\seeglossary{structured goal}.  Internally, an Isar proof state is
wenzelm@20472
    21
organized as a stack to accomodate block structure of proof texts.
wenzelm@20472
    22
For historical reasons, a low-level \seeglossary{tactical goal} is
wenzelm@20472
    23
occasionally called ``proof state'' as well.}
wenzelm@20472
    24
wenzelm@20472
    25
\glossary{Structured goal}{FIXME}
wenzelm@20472
    26
wenzelm@20472
    27
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
wenzelm@20472
    28
wenzelm@20472
    29
wenzelm@20472
    30
*}
wenzelm@20472
    31
wenzelm@20472
    32
section {* Proof methods *}
wenzelm@20472
    33
wenzelm@20472
    34
text FIXME
wenzelm@20472
    35
wenzelm@20472
    36
section {* Attributes *}
wenzelm@20472
    37
wenzelm@20472
    38
text "FIXME ?!"
wenzelm@20472
    39
wenzelm@20472
    40
wenzelm@20472
    41
end