renamed kill_all to kill, in conformance with atp_kill command;
simplified/unified treatment of preferences;
check_thread_manager: CRITICAL due to global ref;
goal addressing via Thm.cprem_of;
reduced NJ basis library stuff to bare minimum;
(* $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