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