--- a/doc-src/TutorialI/Rules/Basic.thy Mon Dec 16 13:43:11 2002 +0100
+++ b/doc-src/TutorialI/Rules/Basic.thy Tue Dec 17 11:04:30 2002 +0100
@@ -186,9 +186,38 @@
oops
+text{*unification failure trace *}
+
+ML "set trace_unify_fail"
+
+lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+apply assumption
+Clash: e =/= c
+
+Clash: == =/= Trueprop
+*}
+oops
+
+lemma "\<forall>x y. P(x,y) --> P(y,x)"
+apply auto
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+apply assumption
+
+Clash: bound variable x (depth 1) =/= bound variable y (depth 0)
+
+Clash: == =/= Trueprop
+Clash: == =/= Trueprop
+*}
+oops
+
+ML "reset trace_unify_fail"
+
+
text{*Quantifiers*}
-
text {*
@{thm[display] allI}
\rulename{allI}