diff -r 558615299200 -r 310e9b810bbf src/Doc/IsarRef/ML_Tactic.thy
--- a/src/Doc/IsarRef/ML_Tactic.thy	Sun Nov 04 20:11:05 2012 +0100
+++ b/src/Doc/IsarRef/ML_Tactic.thy	Sun Nov 04 20:11:19 2012 +0100
@@ -80,13 +80,11 @@
 
 section {* Simplifier tactics *}
 
-text {*
-  The main Simplifier tactics @{ML simp_tac} and variants (cf.\
-  \cite{isabelle-ref}) are all covered by the @{method simp} and
-  @{method simp_all} methods (see \secref{sec:simplifier}).  Note that
-  there is no individual goal addressing available, simplification
-  acts either on the first goal (@{method simp}) or all goals
-  (@{method simp_all}).
+text {* The main Simplifier tactics @{ML simp_tac} and variants are
+  all covered by the @{method simp} and @{method simp_all} methods
+  (see \secref{sec:simplifier}).  Note that there is no individual
+  goal addressing available, simplification acts either on the first
+  goal (@{method simp}) or all goals (@{method simp_all}).
 
   \medskip
   \begin{tabular}{lll}