# HG changeset patch
# User wenzelm
# Date 1234550474 -3600
# Node ID 1da96affdefe822471f0585b3165039cb93d8003
# Parent  fe5ceb6e9a7daee6698c01c35db0e8dec102f2ba
misc tuning;

diff -r fe5ceb6e9a7d -r 1da96affdefe doc-src/IsarRef/Thy/First_Order_Logic.thy
--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Thu Feb 12 22:23:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Fri Feb 13 19:41:14 2009 +0100
@@ -162,7 +162,7 @@
   (\secref{sec:simplifier}), the main automated tool for equational
   reasoning in Isabelle.  Then ``@{command unfolding}~@{thm
   left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
-  "(simp add: left_inv)"}'' etc.
+  "(simp only: left_inv)"}'' etc.
 *}
 
 end
@@ -311,16 +311,17 @@
 qed
 
 text {*
-  These examples illustrate both classical reasoning and non-trivial
-  propositional proofs in general.  All three rules characterize
-  classical logic independently, but the original rule is already the
-  most convenient to use, because it leaves the conclusion unchanged.
-  Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
-  eliminations, despite the additional twist that the context refers
-  to the main conclusion.  So we may write @{thm classical} as the
-  Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''.  This also
-  explains nicely how classical reasoning really works: whatever the
-  main @{text thesis} might be, we may always assume its negation!
+  \noindent These examples illustrate both classical reasoning and
+  non-trivial propositional proofs in general.  All three rules
+  characterize classical logic independently, but the original rule is
+  already the most convenient to use, because it leaves the conclusion
+  unchanged.  Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our
+  format for eliminations, despite the additional twist that the
+  context refers to the main conclusion.  So we may write @{thm
+  classical} as the Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''.
+  This also explains nicely how classical reasoning really works:
+  whatever the main @{text thesis} might be, we may always assume its
+  negation!
 *}
 
 end
@@ -348,10 +349,10 @@
   exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
 
 text {*
-  \noindent The @{thm exE} rule corresponds to an Isar statement
-  ``@{text "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}''.  In the
-  following example we illustrate quantifier reasoning with all four
-  rules:
+  \noindent The statement of @{thm exE} corresponds to ``@{text
+  "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar.  In the
+  subsequent example we illustrate quantifier reasoning involving all
+  four rules:
 *}
 
 theorem
@@ -401,9 +402,10 @@
   \noindent This essentially provides a declarative reading of Pure
   rules as Isar reasoning patterns: the rule statements tells how a
   canonical proof outline shall look like.  Since the above rules have
-  already been declared as @{attribute intro}, @{attribute elim},
-  @{attribute dest} --- each according to its particular shape --- we
-  can immediately write Isar proof texts as follows.
+  already been declared as @{attribute (Pure) intro}, @{attribute
+  (Pure) elim}, @{attribute (Pure) dest} --- each according to its
+  particular shape --- we can immediately write Isar proof texts as
+  follows:
 *}
 
 (*<*)
diff -r fe5ceb6e9a7d -r 1da96affdefe doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Thu Feb 12 22:23:09 2009 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy	Fri Feb 13 19:41:14 2009 +0100
@@ -9,7 +9,7 @@
   \cite{Wenzel:1999:TPHOL,Wenzel-PhD,Nipkow-TYPES02,Wenzel-Paulson:2006,Wenzel:2006:Festschrift}
   is intended as a generic framework for developing formal
   mathematical documents with full proof checking.  Definitions and
-  proofs are organized as theories; an assembly of theory sources may
+  proofs are organized as theories.  An assembly of theory sources may
   be presented as a printed document; see also
   \chref{ch:document-prep}.
 
@@ -29,7 +29,7 @@
   formal proofs directly as objects of some logical calculus (e.g.\
   @{text "\<lambda>"}-terms in a version of type theory).  In fact, Isar is
   better understood as an interpreter of a simple block-structured
-  language for describing data flow of local facts and goals,
+  language for describing the data flow of local facts and goals,
   interspersed with occasional invocations of proof methods.
   Everything is reduced to logical inferences internally, but these
   steps are somewhat marginal compared to the overall bookkeeping of
@@ -52,28 +52,28 @@
   \cite{isabelle-ZF} is less extensively developed, although it would
   probably fit better for classical mathematics.
 
-  \medskip In order to illustrate typical natural deduction reasoning
-  in Isar, we shall refer to the background theory and library of
-  Isabelle/HOL.  This includes common notions of predicate logic,
-  naive set-theory etc.\ using fairly standard mathematical notation.
-  From the perspective of generic natural deduction there is nothing
-  special about the logical connectives of HOL (@{text "\<and>"}, @{text
-  "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"}, etc.), only the resulting reasoning
-  principles are relevant to the user.  There are similar rules
-  available for set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text
-  "\<Inter>"}, @{text "\<Union>"}, etc.), or any other theory developed in the
-  library (lattice theory, topology etc.).
+  \medskip In order to illustrate natural deduction in Isar, we shall
+  refer to the background theory and library of Isabelle/HOL.  This
+  includes common notions of predicate logic, naive set-theory etc.\
+  using fairly standard mathematical notation.  From the perspective
+  of generic natural deduction there is nothing special about the
+  logical connectives of HOL (@{text "\<and>"}, @{text "\<or>"}, @{text "\<forall>"},
+  @{text "\<exists>"}, etc.), only the resulting reasoning principles are
+  relevant to the user.  There are similar rules available for
+  set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text "\<Inter>"}, @{text
+  "\<Union>"}, etc.), or any other theory developed in the library (lattice
+  theory, topology etc.).
 
   Subsequently we briefly review fragments of Isar proof texts
-  corresponding directly to such general natural deduction schemes.
-  The examples shall refer to set-theory, to minimize the danger of
+  corresponding directly to such general deduction schemes.  The
+  examples shall refer to set-theory, to minimize the danger of
   understanding connectives of predicate logic as something special.
 
   \medskip The following deduction performs @{text "\<inter>"}-introduction,
   working forwards from assumptions towards the conclusion.  We give
   both the Isar text, and depict the primitive rule involved, as
-  determined by unification of the problem against rules from the
-  context.
+  determined by unification of the problem against rules that are
+  declared in the library context.
 *}
 
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
@@ -97,11 +97,11 @@
 text_raw {*\end{minipage}*}
 
 text {*
-  \medskip\noindent Note that @{command "assume"} augments the
-  context, @{command "then"} indicates that the current facts shall be
-  used in the next step, and @{command "have"} states a local claim.
-  The two dots ``@{command ".."}'' above refer to a complete proof of
-  the claim, using the indicated facts and a canonical rule from the
+  \medskip\noindent Note that @{command "assume"} augments the proof
+  context, @{command "then"} indicates that the current fact shall be
+  used in the next step, and @{command "have"} states an intermediate
+  goal.  The two dots ``@{command ".."}'' refer to a complete proof of
+  this claim, using the indicated facts and a canonical rule from the
   context.  We could have been more explicit here by spelling out the
   final proof step via the @{command "by"} command:
 *}
@@ -119,12 +119,12 @@
 text {*
   \noindent The format of the @{text "\<inter>"}-introduction rule represents
   the most basic inference, which proceeds from given premises to a
-  conclusion, without any additional context involved.
+  conclusion, without any nested proof context involved.
 
-  \medskip The next example performs backwards introduction on @{term
-  "\<Inter>\<A>"}, the intersection of all sets within a given set.  This
-  requires a nested proof of set membership within a local context of
-  an arbitrary-but-fixed member of the collection:
+  The next example performs backwards introduction on @{term "\<Inter>\<A>"},
+  the intersection of all sets within a given set.  This requires a
+  nested proof of set membership within a local context, where @{term
+  A} is an arbitrary-but-fixed member of the collection:
 *}
 
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
@@ -156,7 +156,7 @@
   primitive rule depicted above.  The system determines it in the
   ``@{command "proof"}'' step, which could have been spelt out more
   explicitly as ``@{command "proof"}~@{text "(rule InterI)"}''.  Note
-  that this rule involves both a local parameter @{term "A"} and an
+  that the rule involves both a local parameter @{term "A"} and an
   assumption @{prop "A \<in> \<A>"} in the nested reasoning.  This kind of
   compound rule typically demands a genuine sub-proof in Isar, working
   backwards rather than forwards as seen before.  In the proof body we
@@ -234,16 +234,29 @@
   The Pure logic \cite{paulson-found,paulson700} is an intuitionistic
   fragment of higher-order logic \cite{church40}.  In type-theoretic
   parlance, there are three levels of @{text "\<lambda>"}-calculus with
-  corresponding arrows: @{text "\<Rightarrow>"} for syntactic function space
-  (terms depending on terms), @{text "\<And>"} for universal quantification
-  (proofs depending on terms), and @{text "\<Longrightarrow>"} for implication (proofs
-  depending on proofs).
+  corresponding arrows @{text "\<Rightarrow>"}/@{text "\<And>"}/@{text "\<Longrightarrow>"}:
+
+  \medskip
+  \begin{tabular}{ll}
+  @{text "\<alpha> \<Rightarrow> \<beta>"} & syntactic function space (terms depending on terms) \\
+  @{text "\<And>x. B(x)"} & universal quantification (proofs depending on terms) \\
+  @{text "A \<Longrightarrow> B"} & implication (proofs depending on proofs) \\
+  \end{tabular}
+  \medskip
 
-  On top of this, Pure implements a generic calculus for nested
-  natural deduction rules, similar to \cite{Schroeder-Heister:1984}.
-  Here object-logic inferences are internalized as formulae over
-  @{text "\<And>"} and @{text "\<Longrightarrow>"}.  Combining such rule statements may
-  involve higher-order unification \cite{paulson-natural}.
+  \noindent Here only the types of syntactic terms, and the
+  propositions of proof terms have been shown.  The @{text
+  "\<lambda>"}-structure of proofs can be recorded as an optional feature of
+  the Pure inference kernel \cite{Berghofer-Nipkow:2000:TPHOL}, but
+  the formal system can never depend on them due to \emph{proof
+  irrelevance}.
+
+  On top of this most primitive layer of proofs, Pure implements a
+  generic calculus for nested natural deduction rules, similar to
+  \cite{Schroeder-Heister:1984}.  Here object-logic inferences are
+  internalized as formulae over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
+  Combining such rule statements may involve higher-order unification
+  \cite{paulson-natural}.
 *}
 
 
@@ -306,7 +319,7 @@
   rules expressed as formulae, using @{text "\<And>"} to bind local
   parameters and @{text "\<Longrightarrow>"} to express entailment.  Multiple
   parameters and premises are represented by repeating these
-  connectives in a right-associative fashion.
+  connectives in a right-associative manner.
 
   Since @{text "\<And>"} and @{text "\<Longrightarrow>"} commute thanks to the theorem
   @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\
@@ -315,12 +328,26 @@
   nesting.  This means that any Pure proposition may be presented as a
   \emph{Hereditary Harrop Formula} \cite{Miller:1991} which is of the
   form @{text "\<And>x\<^isub>1 \<dots> x\<^isub>m. H\<^isub>1 \<Longrightarrow> \<dots> H\<^isub>n \<Longrightarrow>
-  A"} for @{text "m, n \<ge> 0"}, and @{text "H\<^isub>1, \<dots>, H\<^isub>n"}
-  being recursively of the same format, and @{text "A"} atomic.
+  A"} for @{text "m, n \<ge> 0"}, and @{text "A"} atomic, and @{text
+  "H\<^isub>1, \<dots>, H\<^isub>n"} being recursively of the same format.
   Following the convention that outermost quantifiers are implicit,
   Horn clauses @{text "A\<^isub>1 \<Longrightarrow> \<dots> A\<^isub>n \<Longrightarrow> A"} are a special
   case of this.
 
+  For example, @{text "\<inter>"}-introduction rule encountered before is
+  represented as a Pure theorem as follows:
+  \[
+  @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
+  \]
+
+  \noindent This is a plain Horn clause, since no further nesting on
+  the left is involved.  The general @{text "\<Inter>"}-introduction
+  corresponds to a Hereditary Harrop Formula with one additional level
+  of nesting:
+  \[
+  @{text "InterI:"}~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
+  \]
+
   \medskip Goals are also represented as rules: @{text "A\<^isub>1 \<Longrightarrow>
   \<dots> A\<^isub>n \<Longrightarrow> C"} states that the sub-goals @{text "A\<^isub>1, \<dots>,
   A\<^isub>n"} entail the result @{text "C"}; for @{text "n = 0"} the
@@ -336,10 +363,10 @@
   \end{array}
   \]
 
-  Goal states are refined in intermediate proof steps until a finished
-  form is achieved.  Here the two main reasoning principles are
-  @{inference resolution}, for back-chaining a rule against a sub-goal
-  (replacing it by zero or more sub-goals), and @{inference
+  \noindent Goal states are refined in intermediate proof steps until
+  a finished form is achieved.  Here the two main reasoning principles
+  are @{inference resolution}, for back-chaining a rule against a
+  sub-goal (replacing it by zero or more sub-goals), and @{inference
   assumption}, for solving a sub-goal (finding a short-circuit with
   local assumptions).  Below @{text "\<^vec>x"} stands for @{text
   "x\<^isub>1, \<dots>, x\<^isub>n"} (@{text "n \<ge> 0"}).
@@ -371,8 +398,9 @@
   The following trace illustrates goal-oriented reasoning in
   Isabelle/Pure:
 
+  {\footnotesize
   \medskip
-  \begin{tabular}{r@ {\qquad}l}
+  \begin{tabular}{r@ {\quad}l}
   @{text "(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)"} & @{text "(init)"} \\
   @{text "(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)"} \\
   @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> B)"} \\
@@ -382,6 +410,7 @@
   @{text "A \<and> B \<Longrightarrow> B \<and> A"} & @{text "(finish)"} \\
   \end{tabular}
   \medskip
+  }
 
   Compositions of @{inference assumption} after @{inference
   resolution} occurs quite often, typically in elimination steps.
@@ -411,6 +440,11 @@
   main @{command "fix"}-@{command "assume"}-@{command "show"} skeleton
   of Isar (cf.\ \secref{sec:framework-subproof}): each assumption
   indicated in the text results in a marked premise @{text "G"} above.
+  The marking enforces resolution against one of the sub-goal's
+  premises.  Consequently, @{command "fix"}-@{command
+  "assume"}-@{command "show"} enables to fit the result of a sub-proof
+  quite robustly into a pending sub-goal, while maintaining a good
+  measure of flexibility.
 *}
 
 
@@ -459,17 +493,18 @@
   "term"} with schematic variables, to be bound by higher-order
   matching.
 
-  \medskip Facts may be referenced by name or proposition.  E.g.\ the
-  result of ``@{command "have"}~@{text "a: A \<langle>proof\<rangle>"}'' becomes
-  available both as @{text "a"} and \isacharbackquoteopen@{text
-  "A"}\isacharbackquoteclose.  Moreover, fact expressions may involve
-  attributes that modify either the theorem or the background context.
-  For example, the expression ``@{text "a [OF b]"}'' refers to the
-  composition of two facts according to the @{inference resolution}
-  inference of \secref{sec:framework-resolution}, while ``@{text "a
-  [intro]"}'' declares a fact as introduction rule in the context.
+  \medskip Facts may be referenced by name or proposition.  For
+  example, the result of ``@{command "have"}~@{text "a: A \<langle>proof\<rangle>"}''
+  becomes available both as @{text "a"} and
+  \isacharbackquoteopen@{text "A"}\isacharbackquoteclose.  Moreover,
+  fact expressions may involve attributes that modify either the
+  theorem or the background context.  For example, the expression
+  ``@{text "a [OF b]"}'' refers to the composition of two facts
+  according to the @{inference resolution} inference of
+  \secref{sec:framework-resolution}, while ``@{text "a [intro]"}''
+  declares a fact as introduction rule in the context.
 
-  The special fact name ``@{fact this}'' always refers to the last
+  The special fact called ``@{fact this}'' always refers to the last
   result, as produced by @{command note}, @{text "\<ASSM>"}, @{command
   "have"}, or @{command "show"}.  Since @{command "note"} occurs
   frequently together with @{command "then"} we provide some
@@ -493,13 +528,13 @@
   @{attribute (Pure) dest}, followed by those declared as @{attribute
   (Pure) intro}.
 
-  The default method for @{command "proof"} is ``@{method default}''
+  The default method for @{command "proof"} is ``@{method rule}''
   (arguments picked from the context), for @{command "qed"} it is
   ``@{method "-"}''.  Further abbreviations for terminal proof steps
   are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
   ``@{command "proof"}~@{text "method\<^sub>1"}~@{command
   "qed"}~@{text "method\<^sub>2"}'', and ``@{command ".."}'' for
-  ``@{command "by"}~@{method default}, and ``@{command "."}'' for
+  ``@{command "by"}~@{method rule}, and ``@{command "."}'' for
   ``@{command "by"}~@{method this}''.  The @{command "unfolding"}
   element operates directly on the current facts and goal by applying
   equalities.
@@ -525,18 +560,18 @@
 text {*
   In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"}
   essentially acts like a proof context.  Isar elaborates this idea
-  towards a higher-level notion, with separate information for
+  towards a higher-level notion, with additional information for
   type-inference, term abbreviations, local facts, hypotheses etc.
 
   The element @{command "fix"}~@{text "x :: \<alpha>"} declares a local
   parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
   results exported from the context, @{text "x"} may become anything.
   The @{text "\<ASSM>"} element provides a general interface to
-  hypotheses: ``@{text "\<ASSM> \<guillemotleft>rule\<guillemotright> A"}'' produces @{text "A \<turnstile> A"}
-  locally, while the included inference rule tells how to discharge
+  hypotheses: ``@{text "\<ASSM> \<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile>
+  A"} locally, while the included inference tells how to discharge
   @{text "A"} from results @{text "A \<turnstile> B"} later on.  There is no
-  user-syntax for @{text "\<guillemotleft>rule\<guillemotright>"}, i.e.\ @{text "\<ASSM>"} may only
-  occur in derived elements that provide a suitable inference
+  user-syntax for @{text "\<guillemotleft>inference\<guillemotright>"}, i.e.\ @{text "\<ASSM>"} may
+  only occur in derived elements that provide a suitable inference
   internally.  In particular, ``@{command "assume"}~@{text A}''
   abbreviates ``@{text "\<ASSM> \<guillemotleft>discharge\<guillemotright> A"}'', and ``@{command
   "def"}~@{text "x \<equiv> a"}'' abbreviates ``@{command "fix"}~@{text "x
@@ -603,31 +638,27 @@
 theorem True
 proof
 (*>*)
-  txt_raw {* \begin{minipage}{0.22\textwidth} *}
+  txt_raw {* \begin{minipage}[t]{0.4\textwidth} *}
   {
     fix x
-    have "B x"
-      sorry %noproof
+    have "B x" sorry %noproof
   }
   note `\<And>x. B x`
-  txt_raw {* \end{minipage}\quad\begin{minipage}{0.22\textwidth} *}(*<*)next(*>*)
+  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+  {
+    assume A
+    have B sorry %noproof
+  }
+  note `A \<Longrightarrow> B`
+  txt_raw {* \end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
   {
     def x \<equiv> a
-    have "B x"
-      sorry %noproof
+    have "B x" sorry %noproof
   }
   note `B a`
-  txt_raw {* \end{minipage}\quad\begin{minipage}{0.22\textwidth} *}(*<*)next(*>*)
+  txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
   {
-    assume A
-    have B
-      sorry %noproof
-  }
-  note `A \<Longrightarrow> B`
-  txt_raw {* \end{minipage}\quad\begin{minipage}{0.34\textwidth} *}(*<*)next(*>*)
-  {
-    obtain x
-      where "A x" sorry %noproof
+    obtain x where "A x" sorry %noproof
     have B sorry %noproof
   }
   note `B`
@@ -652,7 +683,8 @@
   & @{text "|"} & @{text "\<ASSUMES> name: props \<AND> \<dots>"} \\
 
   @{text "conclusion"} & @{text "\<equiv>"} & @{text "\<SHOWS> name: props \<AND> \<dots>"} \\
-  & @{text "|"} & @{text "\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>   \<BBAR>   \<dots>"}
+  & @{text "|"} & @{text "\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>"} \\
+  & & \quad @{text "\<BBAR> \<dots>"} \\
   \end{tabular}
 
   \medskip\noindent A simple @{text "statement"} consists of named
@@ -754,10 +786,11 @@
   linguistic mode, goal state, and inferences:
 *}
 
+text_raw {* \begingroup\footnotesize *}
 (*<*)lemma True
 proof
 (*>*)
-  txt_raw {* \begin{minipage}[t]{0.15\textwidth} *}
+  txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
   have "A \<longrightarrow> B"
   proof
     assume A
@@ -765,7 +798,7 @@
       sorry %noproof
   qed
   txt_raw {* \end{minipage}\quad
-\begin{minipage}[t]{0.07\textwidth}
+\begin{minipage}[t]{0.06\textwidth}
 @{text "begin"} \\
 \\
 \\
@@ -780,16 +813,16 @@
 @{text "prove"} \\
 @{text "state"} \\
 @{text "state"} \\
-\end{minipage}\begin{minipage}[t]{0.3\textwidth}
+\end{minipage}\begin{minipage}[t]{0.35\textwidth}
 @{text "(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
 @{text "(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
 \\
 \\
 @{text "#(A \<longrightarrow> B)"} \\
 @{text "A \<longrightarrow> B"} \\
-\end{minipage}\begin{minipage}[t]{0.35\textwidth}
+\end{minipage}\begin{minipage}[t]{0.4\textwidth}
 @{text "(init)"} \\
-@{text "(resolution (A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B)"} \\
+@{text "(resolution impI)"} \\
 \\
 \\
 @{text "(refinement #A \<Longrightarrow> B)"} \\
@@ -798,9 +831,10 @@
 (*<*)
 qed
 (*>*)
+text_raw {* \endgroup *}
 
 text {*
-  Here the @{inference refinement} inference from
+  \noindent Here the @{inference refinement} inference from
   \secref{sec:framework-resolution} mediates composition of Isar
   sub-proofs nicely.  Observe that this principle incorporates some
   degree of freedom in proof composition.  In particular, the proof
@@ -835,7 +869,7 @@
     show "C x y" sorry %noproof
   qed
 
-txt_raw {*\end{minipage} \\[\medskipamount] \begin{minipage}{0.5\textwidth}*}
+txt_raw {*\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}*}
 
 (*<*)
 next
@@ -864,7 +898,7 @@
 text_raw {*\end{minipage}*}
 
 text {*
-  \medskip Such ``peephole optimizations'' of Isar texts are
+  \medskip\noindent Such ``peephole optimizations'' of Isar texts are
   practically important to improve readability, by rearranging
   contexts elements according to the natural flow of reasoning in the
   body, while still observing the overall scoping rules.
@@ -881,7 +915,7 @@
 subsection {* Calculational reasoning \label{sec:framework-calc} *}
 
 text {*
-  The present Isar infrastructure is sufficiently flexible to support
+  The existing Isar infrastructure is sufficiently flexible to support
   calculational reasoning (chains of transitivity steps) as derived
   concept.  The generic proof elements introduced below depend on
   rules declared as @{attribute trans} in the context.  It is left to
@@ -894,16 +928,16 @@
   and \cite{Bauer-Wenzel:2001}.
 
   The generic calculational mechanism is based on the observation that
-  rules such as @{text "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the
-  premises towards the conclusion in a deterministic fashion.  Thus we
-  may reason in forward mode, feeding intermediate results into rules
-  selected from the context.  The course of reasoning is organized by
-  maintaining a secondary fact called ``@{fact calculation}'', apart
-  from the primary ``@{fact this}'' already provided by the Isar
-  primitives.  In the definitions below, @{attribute OF} refers to
-  @{inference resolution} (\secref{sec:framework-resolution}) with
-  multiple rule arguments, and @{text "trans"} represents to a
-  suitable rule from the context:
+  rules such as @{text "trans:"}~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}
+  proceed from the premises towards the conclusion in a deterministic
+  fashion.  Thus we may reason in forward mode, feeding intermediate
+  results into rules selected from the context.  The course of
+  reasoning is organized by maintaining a secondary fact called
+  ``@{fact calculation}'', apart from the primary ``@{fact this}''
+  already provided by the Isar primitives.  In the definitions below,
+  @{attribute OF} refers to @{inference resolution}
+  (\secref{sec:framework-resolution}) with multiple rule arguments,
+  and @{text "trans"} represents to a suitable rule from the context:
 
   \begin{matharray}{rcl}
     @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\