src/HOL/Hoare_Parallel/Graph.thy

--- a/src/HOL/Hoare_Parallel/Graph.thy	Fri Feb 25 08:46:52 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Fri Feb 25 14:25:41 2011 +0100
@@ -140,11 +140,8 @@
 apply simp
 apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
  prefer 2 apply arith
-apply(drule nth_drop)
-apply simp
 apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
  prefer 2 apply arith 
-apply simp
 apply clarify
 apply(case_tac "i")
  apply(force simp add: nth_list_update)