diff -r 7e491da6bcbd -r e08cc8b20564 src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sat Nov 03 21:31:40 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 04 19:05:34 2012 +0100
@@ -496,6 +496,7 @@
   \end{tabular}
   \end{center}
 
+  %FIXME move?
   \medskip The Splitter package is usually configured to work as part
   of the Simplifier.  The effect of repeatedly applying @{ML
   split_tac} can be simulated by ``@{text "(simp only: split:
@@ -504,6 +505,95 @@
 *}
 
 
+subsubsection {* Examples *}
+
+text {* We consider basic algebraic simplifications in Isabelle/HOL.
+  The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like
+  a good candidate to be solved by a single call of @{method simp}:
+*}
+
+lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
+
+text {* The above attempt \emph{fails}, because @{term "0"} and @{term
+  "op +"} in the HOL library are declared as generic type class
+  operations, without stating any algebraic laws yet.  More specific
+  types are required to get access to certain standard simplifications
+  of the theory context, e.g.\ like this: *}
+
+lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp
+lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp
+lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp
+
+text {*
+  \medskip In many cases, assumptions of a subgoal are also needed in
+  the simplification process.  For example:
+*}
+
+lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp
+lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops
+lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp
+
+text {* As seen above, local assumptions that shall contribute to
+  simplification need to be part of the subgoal already, or indicated
+  explicitly for use by the subsequent method invocation.  Both too
+  little or too much information can make simplification fail, for
+  different reasons.
+
+  In the next example the malicious assumption @{prop "\<And>x::nat. f x =
+  g (f (g x))"} does not contribute to solve the problem, but makes
+  the default @{method simp} method loop: the rewrite rule @{text "f
+  ?x \<equiv> g (f (g ?x))"} extracted from the assumption does not
+  terminate.  The Simplifier notices certain simple forms of
+  nontermination, but not this one.  The problem can be solved
+  nonetheless, by ignoring assumptions via special options as
+  explained before:
+*}
+
+lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0"
+  by (simp (no_asm))
+
+text {* The latter form is typical for long unstructured proof
+  scripts, where the control over the goal content is limited.  In
+  structured proofs it is usually better to avoid pushing too many
+  facts into the goal state in the first place.  Assumptions in the
+  Isar proof context do not intrude the reasoning if not used
+  explicitly.  This is illustrated for a toplevel statement and a
+  local proof body as follows:
+*}
+
+lemma
+  assumes "\<And>x::nat. f x = g (f (g x))"
+  shows "f 0 = f 0 + 0" by simp
+
+notepad
+begin
+  assume "\<And>x::nat. f x = g (f (g x))"
+  have "f 0 = f 0 + 0" by simp
+end
+
+text {* \medskip Because assumptions may simplify each other, there
+  can be very subtle cases of nontermination. For example, the regular
+  @{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y
+  \<Longrightarrow> Q"} gives rise to the infinite reduction sequence
+  \[
+  @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto}
+  @{text "P (f y)"} \stackrel{@{text "y \<equiv> x"}}{\longmapsto}
+  @{text "P (f x)"} \stackrel{@{text "f x \<equiv> f y"}}{\longmapsto} \cdots
+  \]
+  whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow>
+  Q"} terminates (without solving the goal):
+*}
+
+lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
+  apply simp
+  oops
+
+text {* See also \secref{sec:simp-config} for options to enable
+  Simplifier trace mode, which often helps to diagnose problems with
+  rewrite systems.
+*}
+
+
 subsection {* Declaring rules \label{sec:simp-rules} *}
 
 text {*