diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/Thy/Logic.thy --- 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 "\"}-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 \ 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 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 "\"}. *} + subsection {* Primitive connectives and rules \label{sec:prim-rules} *} 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 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 = (\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 top-level + structure is merely that of a Horn Clause. \[