# HG changeset patch
# User wenzelm
# Date 1352056279 -3600
# Node ID 310e9b810bbf02f3b3e6ca0f8de0e6ebfcba318a
# Parent  558615299200c7175def1d6c51bf7b2022e3ce52
tuned;

diff -r 558615299200 -r 310e9b810bbf src/Doc/IsarRef/Generic.thy
--- 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.
 
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}