--- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:11:05 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:11:19 2012 +0100
@@ -849,7 +849,7 @@
Note that forward simplification restricts the simplifier to its
most basic operation of term rewriting; solver and looper tactics
- \cite{isabelle-ref} are \emph{not} involved here. The @{text
+ \cite{isabelle-ref} are \emph{not} involved here. The @{attribute
simplified} attribute should be only rarely required under normal
circumstances.
--- 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}