--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/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 simply-typed @{text "\<lambda>"}-calculus
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
or \cite{paulson-ml2}), 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 \<Longrightarrow> B"} or universal quantification @{text
- "\<And>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 "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; 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 extra-logical 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 arbitrary-but-fixed 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 well-typed 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 "\<equiv>"}.
*}
+
subsection {* Primitive connectives and rules \label{sec:prim-rules} *}
text {*
@@ -801,16 +763,13 @@
expect a normal form: quantifiers @{text "\<And>"} before implications
@{text "\<Longrightarrow>"} at each level of nesting.
-\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
-format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
-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 \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost
-quantifier prefix is represented via \seeglossary{schematic
-variables}, such that the top-level 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 = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow> 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 \<Longrightarrow> (\<And>x. B x)) \<equiv>
+ (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost quantifier prefix is
+ represented via schematic variables, such that the top-level
+ structure is merely that of a Horn Clause.
\[