diff -r 5c36db9db335 -r 200f749c96db src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sat Nov 10 20:16:16 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 11 16:19:55 2012 +0100
@@ -766,6 +766,105 @@
 *}
 
 
+subsection {* Ordered rewriting with permutative rules *}
+
+text {* A rewrite rule is \emph{permutative} if the left-hand side and
+  right-hand side are the equal up to renaming of variables.  The most
+  common permutative rule is commutativity: @{text "?x + ?y = ?y +
+  ?x"}.  Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) -
+  ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y
+  (insert ?x ?A)"} for sets.  Such rules are common enough to merit
+  special attention.
+
+  Because ordinary rewriting loops given such rules, the Simplifier
+  employs a special strategy, called \emph{ordered rewriting}.
+  Permutative rules are detected and only applied if the rewriting
+  step decreases the redex wrt.\ a given term ordering.  For example,
+  commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then
+  stops, because the redex cannot be decreased further in the sense of
+  the term ordering.
+
+  The default is lexicographic ordering of term structure, but this
+  could be also changed locally for special applications via
+  @{index_ML Simplifier.set_termless} in Isabelle/ML.
+
+  \medskip Permutative rewrite rules are declared to the Simplifier
+  just like other rewrite rules.  Their special status is recognized
+  automatically, and their application is guarded by the term ordering
+  accordingly. *}
+
+
+subsubsection {* Rewriting with AC operators *}
+
+text {* Ordered rewriting is particularly effective in the case of
+  associative-commutative operators.  (Associativity by itself is not
+  permutative.)  When dealing with an AC-operator @{text "f"}, keep
+  the following points in mind:
+
+  \begin{itemize}
+
+  \item The associative law must always be oriented from left to
+  right, namely @{text "f (f x y) z = f x (f y z)"}.  The opposite
+  orientation, if used with commutativity, leads to looping in
+  conjunction with the standard term order.
+
+  \item To complete your set of rewrite rules, you must add not just
+  associativity (A) and commutativity (C) but also a derived rule
+  \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.
+
+  \end{itemize}
+
+  Ordered rewriting with the combination of A, C, and LC sorts a term
+  lexicographically --- the rewriting engine imitates bubble-sort.
+*}
+
+locale AC_example =
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
+  assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
+  assumes commute: "x \<bullet> y = y \<bullet> x"
+begin
+
+lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"
+proof -
+  have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> z" by (simp only: commute)
+  then show ?thesis by (simp only: assoc)
+qed
+
+lemmas AC_rules = assoc commute left_commute
+
+text {* Thus the Simplifier is able to establish equalities with
+  arbitrary permutations of subterms, by normalizing to a common
+  standard form.  For example: *}
+
+lemma "(b \<bullet> c) \<bullet> a = xxx"
+  apply (simp only: AC_rules)
+  txt {* @{subgoals} *}
+  oops
+
+lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules)
+lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules)
+lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> a" by (simp only: AC_rules)
+
+end
+
+text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and
+  give many examples; other algebraic structures are amenable to
+  ordered rewriting, such as boolean rings.  The Boyer-Moore theorem
+  prover \cite{bm88book} also employs ordered rewriting.
+*}
+
+
+subsubsection {* Re-orienting equalities *}
+
+text {* Another application of ordered rewriting uses the derived rule
+  @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to
+  reverse equations.
+
+  This is occasionally useful to re-orient local assumptions according
+  to the term ordering, when other built-in mechanisms of
+  reorientation and mutual simplification fail to apply.  *}
+
+
 subsection {* Configuration options \label{sec:simp-config} *}
 
 text {*