doc-src/TutorialI/Advanced/simp.thy

 sides.  They may not contain extraneous term or type variables, though.
 *}
 
 subsubsection{*The preprocessor*}
 
-text{*
+text{*\label{sec:simp-preprocessor}
 When some theorem is declared a simplification rule, it need not be a
 conditional equation already.  The simplifier will turn it into a set of
 conditional equations automatically.  For example, given @{prop"f x =
 g x & h x = k x"} the simplifier will turn this into the two separate
 simplifiction rules @{prop"f x = g x"} and @{prop"h x = k x"}. In

 @{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
  P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
 \end{eqnarray}
 Once this conversion process is finished, all remaining non-equations
 $P$ are turned into trivial equations $P = True$.
-For example, the formula @{prop"(p \<longrightarrow> q \<and> r) \<and> s"} is converted into the three rules
+For example, the formula \begin{center}@{prop"(p \<longrightarrow> q \<and> r) \<and> s"}\end{center}
+is converted into the three rules
 \begin{center}
 @{prop"p \<Longrightarrow> q = True"},\quad  @{prop"p \<Longrightarrow> r = True"},\quad  @{prop"s = True"}.
 \end{center}
 \index{simplification rule|)}
 \index{simplification|)}