src/HOL/Hoare/Separation.thy
changeset 44890 22f665a2e91c
parent 44241 7943b69f0188
child 52143 36ffe23b25f8
--- a/src/HOL/Hoare/Separation.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Separation.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -191,7 +191,7 @@
 apply vcg
 apply(simp_all add: star_def ortho_def singl_def)
 
-apply fastsimp
+apply fastforce
 
 apply (clarsimp simp add:List_non_null)
 apply(rename_tac ps')
@@ -214,7 +214,7 @@
 apply(simp)
 apply fast
 
-apply(fastsimp)
+apply(fastforce)
 done
 
 end