src/HOL/Hoare/Separation.thy

   DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD
   {List H q (rev Ps @ Qs)}"
 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')
 apply(rule_tac x = ps' in exI)
 apply(rule_tac x = "p#qs" in exI)

  prefer 2
  apply(blast dest:list_in_heap)
 apply(simp)
 apply fast
 
-apply(fastsimp)
+apply(fastforce)
 done
 
 end