
diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -21,9 +21,9 @@
   DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
   {List tl q (rev Ps @ Qs)}"
 apply vcg_simp
-  apply fastsimp
- apply(fastsimp intro:notin_List_update[THEN iffD2])
-apply fastsimp
+  apply fastforce
+ apply(fastforce intro:notin_List_update[THEN iffD2])
+apply fastforce
 done
 
 end




