# HG changeset patch
# User wenzelm
# Date 1132166059 -3600
# Node ID 54419506df9e8b4c7cde906541f41896f92cf320
# Parent  6e2fd2d276d3aaa71929f4d4988144fea7473cb6
tuned document;

diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -13,10 +13,10 @@
 subsection {* Pure backward reasoning *}
 
 text {*
- In order to get a first idea of how Isabelle/Isar proof documents may
- look like, we consider the propositions $I$, $K$, and $S$.  The
- following (rather explicit) proofs should require little extra
- explanations.
+  In order to get a first idea of how Isabelle/Isar proof documents
+  may look like, we consider the propositions @{text I}, @{text K},
+  and @{text S}.  The following (rather explicit) proofs should
+  require little extra explanations.
 *}
 
 lemma I: "A --> A"
@@ -45,7 +45,7 @@
       assume A
       show C
       proof (rule mp)
-	show "B --> C" by (rule mp)
+        show "B --> C" by (rule mp)
         show B by (rule mp)
       qed
     qed
@@ -53,12 +53,13 @@
 qed
 
 text {*
- Isar provides several ways to fine-tune the reasoning, avoiding
- excessive detail.  Several abbreviated language elements are
- available, enabling the writer to express proofs in a more concise
- way, even without referring to any automated proof tools yet.
+  Isar provides several ways to fine-tune the reasoning, avoiding
+  excessive detail.  Several abbreviated language elements are
+  available, enabling the writer to express proofs in a more concise
+  way, even without referring to any automated proof tools yet.
 
- First of all, proof by assumption may be abbreviated as a single dot.
+  First of all, proof by assumption may be abbreviated as a single
+  dot.
 *}
 
 lemma "A --> A"
@@ -68,11 +69,11 @@
 qed
 
 text {*
- In fact, concluding any (sub-)proof already involves solving any
- remaining goals by assumption\footnote{This is not a completely
- trivial operation, as proof by assumption may involve full
- higher-order unification.}.  Thus we may skip the rather vacuous body
- of the above proof as well.
+  In fact, concluding any (sub-)proof already involves solving any
+  remaining goals by assumption\footnote{This is not a completely
+  trivial operation, as proof by assumption may involve full
+  higher-order unification.}.  Thus we may skip the rather vacuous
+  body of the above proof as well.
 *}
 
 lemma "A --> A"
@@ -80,36 +81,37 @@
 qed
 
 text {*
- Note that the \isacommand{proof} command refers to the $\idt{rule}$
- method (without arguments) by default.  Thus it implicitly applies a
- single rule, as determined from the syntactic form of the statements
- involved.  The \isacommand{by} command abbreviates any proof with
- empty body, so the proof may be further pruned.
+  Note that the \isacommand{proof} command refers to the @{text rule}
+  method (without arguments) by default.  Thus it implicitly applies a
+  single rule, as determined from the syntactic form of the statements
+  involved.  The \isacommand{by} command abbreviates any proof with
+  empty body, so the proof may be further pruned.
 *}
 
 lemma "A --> A"
   by rule
 
 text {*
- Proof by a single rule may be abbreviated as double-dot.
+  Proof by a single rule may be abbreviated as double-dot.
 *}
 
 lemma "A --> A" ..
 
 text {*
- Thus we have arrived at an adequate representation of the proof of a
- tautology that holds by a single standard rule.\footnote{Apparently,
- the rule here is implication introduction.}
+  Thus we have arrived at an adequate representation of the proof of a
+  tautology that holds by a single standard rule.\footnote{Apparently,
+  the rule here is implication introduction.}
 *}
 
 text {*
- Let us also reconsider $K$.  Its statement is composed of iterated
- connectives.  Basic decomposition is by a single rule at a time,
- which is why our first version above was by nesting two proofs.
+  Let us also reconsider @{text K}.  Its statement is composed of
+  iterated connectives.  Basic decomposition is by a single rule at a
+  time, which is why our first version above was by nesting two
+  proofs.
 
- The $\idt{intro}$ proof method repeatedly decomposes a goal's
- conclusion.\footnote{The dual method is $\idt{elim}$, acting on a
- goal's premises.}
+  The @{text intro} proof method repeatedly decomposes a goal's
+  conclusion.\footnote{The dual method is @{text elim}, acting on a
+  goal's premises.}
 *}
 
 lemma "A --> B --> A"
@@ -119,41 +121,40 @@
 qed
 
 text {*
- Again, the body may be collapsed.
+  Again, the body may be collapsed.
 *}
 
 lemma "A --> B --> A"
   by (intro impI)
 
 text {*
- Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof
- methods pick standard structural rules, in case no explicit arguments
- are given.  While implicit rules are usually just fine for single
- rule application, this may go too far with iteration.  Thus in
- practice, $\idt{intro}$ and $\idt{elim}$ would be typically
- restricted to certain structures by giving a few rules only, e.g.\
- \isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip
- implications and universal quantifiers.
+  Just like @{text rule}, the @{text intro} and @{text elim} proof
+  methods pick standard structural rules, in case no explicit
+  arguments are given.  While implicit rules are usually just fine for
+  single rule application, this may go too far with iteration.  Thus
+  in practice, @{text intro} and @{text elim} would be typically
+  restricted to certain structures by giving a few rules only, e.g.\
+  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
+  and universal quantifiers.
 
- Such well-tuned iterated decomposition of certain structures is the
- prime application of $\idt{intro}$ and $\idt{elim}$.  In contrast,
- terminal steps that solve a goal completely are usually performed by
- actual automated proof methods (such as
- \isacommand{by}~$\idt{blast}$).
+  Such well-tuned iterated decomposition of certain structures is the
+  prime application of @{text intro} and @{text elim}.  In contrast,
+  terminal steps that solve a goal completely are usually performed by
+  actual automated proof methods (such as \isacommand{by}~@{text
+  blast}.
 *}
 
 
 subsection {* Variations of backward vs.\ forward reasoning *}
 
 text {*
- Certainly, any proof may be performed in backward-style only.  On the
- other hand, small steps of reasoning are often more naturally
- expressed in forward-style.  Isar supports both backward and forward
- reasoning as a first-class concept.  In order to demonstrate the
- difference, we consider several proofs of $A \conj B \impl B \conj
- A$.
+  Certainly, any proof may be performed in backward-style only.  On
+  the other hand, small steps of reasoning are often more naturally
+  expressed in forward-style.  Isar supports both backward and forward
+  reasoning as a first-class concept.  In order to demonstrate the
+  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
 
- The first version is purely backward.
+  The first version is purely backward.
 *}
 
 lemma "A & B --> B & A"
@@ -167,13 +168,13 @@
 qed
 
 text {*
- Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named
- explicitly, since the goals $B$ and $A$ did not provide any
- structural clue.  This may be avoided using \isacommand{from} to
- focus on $\idt{prems}$ (i.e.\ the $A \conj B$ assumption) as the
- current facts, enabling the use of double-dot proofs.  Note that
- \isacommand{from} already does forward-chaining, involving the
- \name{conjE} rule here.
+  Above, the @{text "conjunct_1/2"} projection rules had to be named
+  explicitly, since the goals @{text B} and @{text A} did not provide
+  any structural clue.  This may be avoided using \isacommand{from} to
+  focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
+  current facts, enabling the use of double-dot proofs.  Note that
+  \isacommand{from} already does forward-chaining, involving the
+  \name{conjE} rule here.
 *}
 
 lemma "A & B --> B & A"
@@ -187,29 +188,29 @@
 qed
 
 text {*
- In the next version, we move the forward step one level upwards.
- Forward-chaining from the most recent facts is indicated by the
- \isacommand{then} command.  Thus the proof of $B \conj A$ from $A
- \conj B$ actually becomes an elimination, rather than an
- introduction.  The resulting proof structure directly corresponds to
- that of the $\name{conjE}$ rule, including the repeated goal
- proposition that is abbreviated as $\var{thesis}$ below.
+  In the next version, we move the forward step one level upwards.
+  Forward-chaining from the most recent facts is indicated by the
+  \isacommand{then} command.  Thus the proof of @{text "B \<and> A"} from
+  @{text "A \<and> B"} actually becomes an elimination, rather than an
+  introduction.  The resulting proof structure directly corresponds to
+  that of the @{text conjE} rule, including the repeated goal
+  proposition that is abbreviated as @{text ?thesis} below.
 *}
 
 lemma "A & B --> B & A"
 proof
   assume "A & B"
   then show "B & A"
-  proof                    -- {* rule \name{conjE} of $A \conj B$ *}
+  proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
     assume A B
-    show ?thesis ..       -- {* rule \name{conjI} of $B \conj A$ *}
+    show ?thesis ..       -- {* rule @{text conjI} of @{text "B \<and> A"} *}
   qed
 qed
 
 text {*
- In the subsequent version we flatten the structure of the main body
- by doing forward reasoning all the time.  Only the outermost
- decomposition step is left as backward.
+  In the subsequent version we flatten the structure of the main body
+  by doing forward reasoning all the time.  Only the outermost
+  decomposition step is left as backward.
 *}
 
 lemma "A & B --> B & A"
@@ -221,9 +222,9 @@
 qed
 
 text {*
- We can still push forward-reasoning a bit further, even at the risk
- of getting ridiculous.  Note that we force the initial proof step to
- do nothing here, by referring to the ``-'' proof method.
+  We can still push forward-reasoning a bit further, even at the risk
+  of getting ridiculous.  Note that we force the initial proof step to
+  do nothing here, by referring to the ``-'' proof method.
 *}
 
 lemma "A & B --> B & A"
@@ -238,29 +239,29 @@
 qed
 
 text {*
- \medskip With these examples we have shifted through a whole range
- from purely backward to purely forward reasoning.  Apparently, in the
- extreme ends we get slightly ill-structured proofs, which also
- require much explicit naming of either rules (backward) or local
- facts (forward).
+  \medskip With these examples we have shifted through a whole range
+  from purely backward to purely forward reasoning.  Apparently, in
+  the extreme ends we get slightly ill-structured proofs, which also
+  require much explicit naming of either rules (backward) or local
+  facts (forward).
 
- The general lesson learned here is that good proof style would
- achieve just the \emph{right} balance of top-down backward
- decomposition, and bottom-up forward composition.  In general, there
- is no single best way to arrange some pieces of formal reasoning, of
- course.  Depending on the actual applications, the intended audience
- etc., rules (and methods) on the one hand vs.\ facts on the other
- hand have to be emphasized in an appropriate way.  This requires the
- proof writer to develop good taste, and some practice, of course.
+  The general lesson learned here is that good proof style would
+  achieve just the \emph{right} balance of top-down backward
+  decomposition, and bottom-up forward composition.  In general, there
+  is no single best way to arrange some pieces of formal reasoning, of
+  course.  Depending on the actual applications, the intended audience
+  etc., rules (and methods) on the one hand vs.\ facts on the other
+  hand have to be emphasized in an appropriate way.  This requires the
+  proof writer to develop good taste, and some practice, of course.
 *}
 
 text {*
- For our example the most appropriate way of reasoning is probably the
- middle one, with conjunction introduction done after elimination.
- This reads even more concisely using \isacommand{thus}, which
- abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same
- vein, \isacommand{hence} abbreviates
- \isacommand{then}~\isacommand{have}.}
+  For our example the most appropriate way of reasoning is probably
+  the middle one, with conjunction introduction done after
+  elimination.  This reads even more concisely using
+  \isacommand{thus}, which abbreviates
+  \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
+  \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
 *}
 
 lemma "A & B --> B & A"
@@ -278,16 +279,16 @@
 subsection {* A few examples from ``Introduction to Isabelle'' *}
 
 text {*
- We rephrase some of the basic reasoning examples of
- \cite{isabelle-intro}, using HOL rather than FOL.
+  We rephrase some of the basic reasoning examples of
+  \cite{isabelle-intro}, using HOL rather than FOL.
 *}
 
 subsubsection {* A propositional proof *}
 
 text {*
- We consider the proposition $P \disj P \impl P$.  The proof below
- involves forward-chaining from $P \disj P$, followed by an explicit
- case-analysis on the two \emph{identical} cases.
+  We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof below
+  involves forward-chaining from @{text "P \<or> P"}, followed by an
+  explicit case-analysis on the two \emph{identical} cases.
 *}
 
 lemma "P | P --> P"
@@ -295,7 +296,7 @@
   assume "P | P"
   thus P
   proof                    -- {*
-    rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
+    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   *}
     assume P show P .
   next
@@ -304,27 +305,27 @@
 qed
 
 text {*
- Case splits are \emph{not} hardwired into the Isar language as a
- special feature.  The \isacommand{next} command used to separate the
- cases above is just a short form of managing block structure.
+  Case splits are \emph{not} hardwired into the Isar language as a
+  special feature.  The \isacommand{next} command used to separate the
+  cases above is just a short form of managing block structure.
 
- \medskip In general, applying proof methods may split up a goal into
- separate ``cases'', i.e.\ new subgoals with individual local
- assumptions.  The corresponding proof text typically mimics this by
- establishing results in appropriate contexts, separated by blocks.
+  \medskip In general, applying proof methods may split up a goal into
+  separate ``cases'', i.e.\ new subgoals with individual local
+  assumptions.  The corresponding proof text typically mimics this by
+  establishing results in appropriate contexts, separated by blocks.
 
- In order to avoid too much explicit parentheses, the Isar system
- implicitly opens an additional block for any new goal, the
- \isacommand{next} statement then closes one block level, opening a
- new one.  The resulting behavior is what one would expect from
- separating cases, only that it is more flexible.  E.g.\ an induction
- base case (which does not introduce local assumptions) would
- \emph{not} require \isacommand{next} to separate the subsequent step
- case.
+  In order to avoid too much explicit parentheses, the Isar system
+  implicitly opens an additional block for any new goal, the
+  \isacommand{next} statement then closes one block level, opening a
+  new one.  The resulting behavior is what one would expect from
+  separating cases, only that it is more flexible.  E.g.\ an induction
+  base case (which does not introduce local assumptions) would
+  \emph{not} require \isacommand{next} to separate the subsequent step
+  case.
 
- \medskip In our example the situation is even simpler, since the two
- cases actually coincide.  Consequently the proof may be rephrased as
- follows.
+  \medskip In our example the situation is even simpler, since the two
+  cases actually coincide.  Consequently the proof may be rephrased as
+  follows.
 *}
 
 lemma "P | P --> P"
@@ -339,10 +340,10 @@
 qed
 
 text {*
- Again, the rather vacuous body of the proof may be collapsed.  Thus
- the case analysis degenerates into two assumption steps, which are
- implicitly performed when concluding the single rule step of the
- double-dot proof as follows.
+  Again, the rather vacuous body of the proof may be collapsed.  Thus
+  the case analysis degenerates into two assumption steps, which are
+  implicitly performed when concluding the single rule step of the
+  double-dot proof as follows.
 *}
 
 lemma "P | P --> P"
@@ -355,17 +356,17 @@
 subsubsection {* A quantifier proof *}
 
 text {*
- To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
- x)) \impl (\ex x P \ap x)$.  Informally, this holds because any $a$
- with $P \ap (f \ap a)$ may be taken as a witness for the second
- existential statement.
+  To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
+  x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any @{text a}
+  with @{text "P (f a)"} may be taken as a witness for the second
+  existential statement.
 
- The first proof is rather verbose, exhibiting quite a lot of
- (redundant) detail.  It gives explicit rules, even with some
- instantiation.  Furthermore, we encounter two new language elements:
- the \isacommand{fix} command augments the context by some new
- ``arbitrary, but fixed'' element; the \isacommand{is} annotation
- binds term abbreviations by higher-order pattern matching.
+  The first proof is rather verbose, exhibiting quite a lot of
+  (redundant) detail.  It gives explicit rules, even with some
+  instantiation.  Furthermore, we encounter two new language elements:
+  the \isacommand{fix} command augments the context by some new
+  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
+  binds term abbreviations by higher-order pattern matching.
 *}
 
 lemma "(EX x. P (f x)) --> (EX y. P y)"
@@ -382,12 +383,12 @@
 qed
 
 text {*
- While explicit rule instantiation may occasionally improve
- readability of certain aspects of reasoning, it is usually quite
- redundant.  Above, the basic proof outline gives already enough
- structural clues for the system to infer both the rules and their
- instances (by higher-order unification).  Thus we may as well prune
- the text as follows.
+  While explicit rule instantiation may occasionally improve
+  readability of certain aspects of reasoning, it is usually quite
+  redundant.  Above, the basic proof outline gives already enough
+  structural clues for the system to infer both the rules and their
+  instances (by higher-order unification).  Thus we may as well prune
+  the text as follows.
 *}
 
 lemma "(EX x. P (f x)) --> (EX y. P y)"
@@ -402,10 +403,10 @@
 qed
 
 text {*
- Explicit $\exists$-elimination as seen above can become quite
- cumbersome in practice.  The derived Isar language element
- ``\isakeyword{obtain}'' provides a more handsome way to do
- generalized existence reasoning.
+  Explicit @{text \<exists>}-elimination as seen above can become quite
+  cumbersome in practice.  The derived Isar language element
+  ``\isakeyword{obtain}'' provides a more handsome way to do
+  generalized existence reasoning.
 *}
 
 lemma "(EX x. P (f x)) --> (EX y. P y)"
@@ -416,13 +417,13 @@
 qed
 
 text {*
- Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
- \isakeyword{assume} together with a soundness proof of the
- elimination involved.  Thus it behaves similar to any other forward
- proof element.  Also note that due to the nature of general existence
- reasoning involved here, any result exported from the context of an
- \isakeyword{obtain} statement may \emph{not} refer to the parameters
- introduced there.
+  Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
+  \isakeyword{assume} together with a soundness proof of the
+  elimination involved.  Thus it behaves similar to any other forward
+  proof element.  Also note that due to the nature of general
+  existence reasoning involved here, any result exported from the
+  context of an \isakeyword{obtain} statement may \emph{not} refer to
+  the parameters introduced there.
 *}
 
 
@@ -430,10 +431,10 @@
 subsubsection {* Deriving rules in Isabelle *}
 
 text {*
- We derive the conjunction elimination rule from the corresponding
- projections.  The proof is quite straight-forward, since
- Isabelle/Isar supports non-atomic goals and assumptions fully
- transparently.
+  We derive the conjunction elimination rule from the corresponding
+  projections.  The proof is quite straight-forward, since
+  Isabelle/Isar supports non-atomic goals and assumptions fully
+  transparently.
 *}
 
 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
@@ -448,12 +449,12 @@
 qed
 
 text {*
- Note that classic Isabelle handles higher rules in a slightly
- different way.  The tactic script as given in \cite{isabelle-intro}
- for the same example of \name{conjE} depends on the primitive
- \texttt{goal} command to decompose the rule into premises and
- conclusion.  The actual result would then emerge by discharging of
- the context at \texttt{qed} time.
+  Note that classic Isabelle handles higher rules in a slightly
+  different way.  The tactic script as given in \cite{isabelle-intro}
+  for the same example of \name{conjE} depends on the primitive
+  \texttt{goal} command to decompose the rule into premises and
+  conclusion.  The actual result would then emerge by discharging of
+  the context at \texttt{qed} time.
 *}
 
 end
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -131,7 +131,7 @@
 
 theorem correctness: "execute (compile e) env = eval e env"
 proof -
-  have "!!stack. exec (compile e) stack env = eval e env # stack"
+  have "\<And>stack. exec (compile e) stack env = eval e env # stack"
   proof (induct e)
     case Variable show ?case by simp
   next
@@ -187,8 +187,7 @@
 
 theorem correctness': "execute (compile e) env = eval e env"
 proof -
-  have exec_compile:
-    "!!stack. exec (compile e) stack env = eval e env # stack"
+  have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
   proof (induct e)
     case (Variable adr s)
     have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -411,36 +411,37 @@
 *}
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
-by (auto simp:Valid_def)
+  by (auto simp add: Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
-by (auto simp:Valid_def)
+  by (auto simp: Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
-by (auto simp:Valid_def)
+  by (auto simp: Valid_def)
 
 lemma CondRule:
- "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
-  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
-by (auto simp:Valid_def)
+  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
+    \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+  by (auto simp: Valid_def)
 
-lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma iter_aux: "
+  \<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
+       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
+  apply(induct n)
+   apply clarsimp
+   apply (simp (no_asm_use))
+   apply blast
+  done
 
 lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
-apply (clarsimp simp:Valid_def)
-apply(drule iter_aux)
-  prefer 2 apply assumption
- apply blast
-apply blast
-done
-
+    "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
+  apply (clarsimp simp: Valid_def)
+  apply (drule iter_aux)
+    prefer 2
+    apply assumption
+   apply blast
+  apply blast
+  done
 
 ML {* val Valid_def = thm "Valid_def" *}
 use "~~/src/HOL/Hoare/hoare.ML"
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -274,31 +274,31 @@
       .{\<acute>S = (SUM j<n. j)}."
   by hoare auto
 
-subsection{*Time*}
+
+subsection{* Time *}
 
 text{*
-A simple embedding of time in Hoare logic: function @{text timeit}
-inserts an extra variable to keep track of the elapsed time.
+  A simple embedding of time in Hoare logic: function @{text timeit}
+  inserts an extra variable to keep track of the elapsed time.
 *}
 
 record tstate = time :: nat
 
-types 'a time = "\<lparr>time::nat, \<dots>::'a\<rparr>"
+types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
 
 consts timeit :: "'a time com \<Rightarrow> 'a time com"
 primrec
-"timeit(Basic f) = (Basic f; Basic(%s. s\<lparr>time := Suc(time s)\<rparr>))"
-"timeit(c1;c2) = (timeit c1; timeit c2)"
-"timeit(Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-"timeit(While b iv c) = While b iv (timeit c)"
-
+  "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
+  "timeit (c1; c2) = (timeit c1; timeit c2)"
+  "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+  "timeit (While b iv c) = While b iv (timeit c)"
 
 record tvars = tstate +
   I :: nat
   J :: nat
 
-lemma lem: "(0::nat) < n \<Longrightarrow> n+n \<le> Suc(n*n)"
-by(induct n, simp_all)
+lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"
+  by (induct n) simp_all
 
 lemma "|- .{i = \<acute>I & \<acute>time = 0}.
  timeit(
@@ -312,17 +312,17 @@
    \<acute>I := \<acute>I - 1
  OD
  ) .{2*\<acute>time = i*i + 5*i}."
-apply simp
-apply hoare
-    apply simp
+  apply simp
+  apply hoare
+      apply simp
+     apply clarsimp
+    apply clarsimp
+   apply arith
+   prefer 2
    apply clarsimp
-  apply clarsimp
+  apply (clarsimp simp: nat_distrib)
+  apply (frule lem)
   apply arith
- prefer 2
- apply clarsimp
-apply (clarsimp simp:nat_distrib)
-apply(frule lem)
-apply arith
-done
+  done
 
 end
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -4,13 +4,15 @@
 theory Puzzle imports Main begin
 
 text_raw {*
- \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
- pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
- Tobias Nipkow.}
+  \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original
+  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by
+  Tobias Nipkow.}
+*}
 
- \medskip \textbf{Problem.}  Given some function $f\colon \Nat \to
- \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all
- $n$.  Demonstrate that $f$ is the identity.
+text {*
+  \textbf{Problem.}  Given some function $f\colon \Nat \to \Nat$ such
+  that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$.
+  Demonstrate that $f$ is the identity.
 *}
 
 theorem
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/Summation.thy	Wed Nov 16 19:34:19 2005 +0100
@@ -113,7 +113,8 @@
 proof (induct n)
   show "?P 0" by simp
 next
-  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" by (simp add: distrib)
+  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
+    by (simp add: distrib)
   also assume "?S n = n * (n + 1) * (2 * n + 1)"
   also have "... + 6 * (n + 1)^Suc (Suc 0) =
     (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/document/root.tex	Wed Nov 16 19:34:19 2005 +0100
@@ -13,11 +13,11 @@
 \maketitle
 
 \begin{abstract}
-  Isar offers a high-level proof (and theory) language for Isabelle.  We give
-  various examples of Isabelle/Isar proof developments, ranging from simple
-  demonstrations of certain language features to a bit more advanced
-  applications.  Note that the ``real'' applications of Isar are found
-  elsewhere.
+  Isar offers a high-level proof (and theory) language for Isabelle.
+  We give various examples of Isabelle/Isar proof developments,
+  ranging from simple demonstrations of certain language features to a
+  bit more advanced applications.  The ``real'' applications of
+  Isabelle/Isar are found elsewhere.
 \end{abstract}
 
 \tableofcontents
diff -r 6e2fd2d276d3 -r 54419506df9e src/HOL/Isar_examples/document/style.tex
--- a/src/HOL/Isar_examples/document/style.tex	Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/document/style.tex	Wed Nov 16 19:34:19 2005 +0100
@@ -3,6 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{ifthen,proof,isabelle,isabellesym}
+\isabellestyle{it}
 \usepackage{pdfsetup}\urlstyle{rm}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
@@ -27,7 +28,7 @@
 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
 \newcommand{\all}[1]{\forall #1\dt\;}
 \newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\impl}{\rightarrow}
+\newcommand{\impl}{\to}
 \newcommand{\conj}{\land}
 \newcommand{\disj}{\lor}
 \newcommand{\Impl}{\Longrightarrow}