diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -31,7 +31,6 @@
   \<^cancel>\<open>apply clarsimp\<close>
   \<^cancel>\<open>apply(rename_tac ps')\<close>
   \<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close>
-  apply fastforce
   done
 
 text\<open>And now with ghost variables \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>. Even
@@ -48,7 +47,6 @@
   {List next q (rev Ps @ Qs)}"
 apply vcg_simp
  apply fastforce
-apply fastforce
 done
 
 text "A longer readable version:"
@@ -104,7 +102,6 @@
 apply vcg_simp
   apply clarsimp
  apply clarsimp
-apply clarsimp
 done
 
 
@@ -461,7 +458,6 @@
 apply (simp only:distPath_def)
 apply vcg_simp
   apply clarsimp
-  apply clarsimp
  apply (case_tac "(q = Null)")
   apply (fastforce intro: Path_is_List)
  apply clarsimp
@@ -499,7 +495,6 @@
   {islist next p \<and> map elem (rev(list next p)) = Xs}"
 apply vcg_simp
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
-apply fastforce
 done