# HG changeset patch
# User wenzelm
# Date 1235153251 -3600
# Node ID cac2ca7bbc08634adfe5ac760f2e880753147225
# Parent  03634a9e91ae5740bb5b7c50b44af1e380c78c48
tuned;

diff -r 03634a9e91ae -r cac2ca7bbc08 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Fri Feb 20 18:48:58 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Feb 20 19:07:31 2009 +0100
@@ -764,7 +764,7 @@
   \]
 
   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
-  hold compound rules of the same shape, not just atomic propositions.
+  again hold compound rules, not just atomic propositions.
   Propositions of this format are called \emph{Hereditary Harrop
   Formulae} in the literature \cite{Miller:1991}.  Here we give an
   inductive characterization as follows:
@@ -777,32 +777,31 @@
   \end{tabular}
   \medskip
 
-  \noindent Thus we essentially impose nesting levels on Pure
-  propositions.  At each level there is a local parameter prefix,
-  followed by premises, and concluding another atomic proposition.
-  Typical examples are implication introduction @{text "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow>
-  B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow>
-  P n"}.  Even deeper nesting occurs in well-founded induction @{text
-  "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this already marks the
-  limit of rule complexity seen in practice.
+  \noindent Thus we essentially impose nesting levels on propositions
+  formed from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a
+  prefix of parameters and compound premises, concluding an atomic
+  proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
+  "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
+  \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
+  induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
+  already marks the limit of rule complexity seen in practice.
 
-  \medskip The main inference system of Isabelle/Pure always maintains
-  the following canonical form of framework propositions:
+  \medskip Regular user-level inferences in Isabelle/Pure always
+  maintain the following canonical form of results:
 
   \begin{itemize}
 
-  \item Results are normalized by means of the equivalence @{prop
-  "(PROP A \<Longrightarrow> (\<And>x. PROP B x)) \<equiv> (\<And>x. PROP A \<Longrightarrow> PROP B x)"}, which is a
-  theorem of Pure.  By pushing quantifiers inside conclusions in front
-  of the implication, we arrive at a normal form that is always a
-  Hereditary Harrop Formula.
+  \item Normalization by the equivalence @{prop "(PROP A \<Longrightarrow> (\<And>x. PROP B
+  x)) \<equiv> (\<And>x. PROP A \<Longrightarrow> PROP B x)"}, which is a theorem of Pure, means
+  that quantifiers are pushed in front of implication at each level of
+  nesting.  The normal form is always a Hereditary Harrop Formula.
 
   \item The outermost prefix of parameters is represented via
-  schematic variables, i.e.\ instead of @{text "\<And>\<^vec>x. \<^vec>H
-  \<^vec>x \<Longrightarrow> A \<^vec>x"} we always work with @{text "\<^vec>H
-  ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.  Note that this representation looses
-  information about the order of parameters, and vacuous quantifiers
-  vanish automatically.
+  schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
+  \<Longrightarrow> A \<^vec>x"} we always have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A
+  ?\<^vec>x"}.  Note that this representation looses information about
+  the order of parameters, and vacuous quantifiers vanish
+  automatically.
 
   \end{itemize}
 *}