src/HOL/HoareParallel/Mul_Gar_Coll.thy
changeset 26316 9e9e67e33557
parent 24742 73b8b42a36b6
child 26342 0f65fa163304
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:29 2008 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:31 2008 +0100
@@ -383,7 +383,7 @@
 apply force
 --{* 1 subgoal left *}
 apply clarify
-apply(drule Nat.le_imp_less_or_eq)
+apply(drule_tac x = "ind x" in le_imp_less_or_eq)
 apply (simp_all add:Blacks_def)
 done