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:
 *}
 
 (*<*)