diff -r 8e127313ed55 -r bdec4a82f385 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Thu Feb 01 20:59:50 2007 +0100
+++ b/src/HOL/HoareParallel/Graph.thy	Fri Feb 02 15:47:58 2007 +0100
@@ -222,7 +222,7 @@
    apply clarify
    apply(rule_tac x = "j" in exI)
    apply(case_tac "Suc i<m")
-    apply(simp add: nth_append min_def)
+    apply(simp add: nth_append)
     apply(case_tac "R=j")
      apply(simp add: nth_list_update)
      apply(case_tac "i=m")
@@ -230,7 +230,7 @@
      apply(erule_tac x = "i" in allE)
      apply force
     apply(force simp add: nth_list_update)
-   apply(simp add: nth_append min_def)
+   apply(simp add: nth_append)
    apply(subgoal_tac "i=m - 1")
     prefer 2 apply arith
    apply(case_tac "R=j")