--- a/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 18:25:54 2005 +0200
@@ -640,6 +640,7 @@
which makes Isabelle show the cause of unification failures (in Proof
General's \textsf{Trace} buffer).
\end{pgnote}
+\noindent
For example, suppose we are trying to prove this subgoal by assumption:
\begin{isabelle}
\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
@@ -648,10 +649,9 @@
\begin{isabelle}
\isacommand{apply} assumption
\end{isabelle}
-Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
+In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
\begin{isabelle}
-Clash: e =/= c\isanewline
-Clash: == =/= Trueprop
+Clash: e =/= c
\end{isabelle}
Isabelle uses