diff r ce2b8e6502f9 r 7a3b5bbed313 docsrc/IsarImplementation/Thy/Logic.thy
 a/docsrc/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:04:15 2009 +0100
+++ b/docsrc/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:23:33 2009 +0100
@@ 186,12 +186,9 @@
*}

section {* Terms \label{sec:terms} *}
text {*
 \glossary{Term}{FIXME}

The language of terms is that of simplytyped @{text "\"}calculus
with deBruijn indices for bound variables (cf.\ \cite{debruijn72}
or \cite{paulsonml2}), with the types being determined determined
@@ 392,42 +389,6 @@
section {* Theorems \label{sec:thms} *}
text {*
 \glossary{Proposition}{FIXME A \seeglossary{term} of
 \seeglossary{type} @{text "prop"}. Internally, there is nothing
 special about propositions apart from their type, but the concrete
 syntax enforces a clear distinction. Propositions are structured
 via implication @{text "A \ B"} or universal quantification @{text
 "\x. B x"}  anything else is considered atomic. The canonical
 form for propositions is that of a \seeglossary{Hereditary Harrop
 Formula}. FIXME}

 \glossary{Theorem}{A proven proposition within a certain theory and
 proof context, formally @{text "\ \\<^sub>\ \"}; both contexts are
 rarely spelled out explicitly. Theorems are usually normalized
 according to the \seeglossary{HHF} format. FIXME}

 \glossary{Fact}{Sometimes used interchangeably for
 \seeglossary{theorem}. Strictly speaking, a list of theorems,
 essentially an extralogical conjunction. Facts emerge either as
 local assumptions, or as results of local goal statements  both
 may be simultaneous, hence the list representation. FIXME}

 \glossary{Schematic variable}{FIXME}

 \glossary{Fixed variable}{A variable that is bound within a certain
 proof context; an arbitrarybutfixed entity within a portion of
 proof text. FIXME}

 \glossary{Free variable}{Synonymous for \seeglossary{fixed
 variable}. FIXME}

 \glossary{Bound variable}{FIXME}

 \glossary{Variable}{See \seeglossary{schematic variable},
 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
 \seeglossary{type variable}. The distinguishing feature of
 different variables is their binding scope. FIXME}

A \emph{proposition} is a welltyped term of type @{text "prop"}, a
\emph{theorem} is a proven proposition (depending on a context of
hypotheses and the background theory). Primitive inferences include
@@ 436,6 +397,7 @@
notion of equality/equivalence @{text "\"}.
*}
+
subsection {* Primitive connectives and rules \label{sec:primrules} *}
text {*
@@ 801,16 +763,13 @@
expect a normal form: quantifiers @{text "\"} before implications
@{text "\"} at each level of nesting.
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
format is defined inductively as @{text "H = (\x\<^sup>*. H\<^sup>* \
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
Any proposition may be put into HHF form by normalizing with the rule
@{text "(A \ (\x. B x)) \ (\x. A \ B x)"}. In Isabelle, the outermost
quantifier prefix is represented via \seeglossary{schematic
variables}, such that the toplevel structure is merely that of a
\seeglossary{Horn Clause}}.

\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
+ The set of propositions in HHF format is defined inductively as
+ @{text "H = (\x\<^sup>*. H\<^sup>* \ A)"}, for variables @{text "x"}
+ and atomic propositions @{text "A"}. Any proposition may be put
+ into HHF form by normalizing with the rule @{text "(A \ (\x. B x)) \
+ (\x. A \ B x)"}. In Isabelle, the outermost quantifier prefix is
+ represented via schematic variables, such that the toplevel
+ structure is merely that of a Horn Clause.
\[