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