# HG changeset patch
# User paulson
# Date 1040119470 -3600
# Node ID 41abb61ecce9a4065d4fb2531c1680f39a9eb13c
# Parent  a9bb54a3cfb7a62d111ef6f789010b460b12d30b
new material for trace_unify_fail

diff -r a9bb54a3cfb7 -r 41abb61ecce9 doc-src/TutorialI/Rules/Basic.thy
--- 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}