changeset 32833 | f3716d1a2e48 |
parent 16417 | 9bc16273c2d4 |
child 32960 | 69916a850301 |
--- a/doc-src/TutorialI/Rules/Basic.thy Thu Oct 01 18:59:26 2009 +0200 +++ b/doc-src/TutorialI/Rules/Basic.thy Thu Oct 01 20:04:44 2009 +0200 @@ -188,7 +188,7 @@ text{*unification failure trace *} -ML "set trace_unify_fail" +ML "Unsynchronized.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{* @@ -213,7 +213,7 @@ *} oops -ML "reset trace_unify_fail" +ML "Unsynchronized.reset trace_unify_fail" text{*Quantifiers*}