| changeset 24742 | 73b8b42a36b6 |
| parent 23894 | 1a4167d761ac |
| child 26316 | 9e9e67e33557 |
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu Sep 27 17:28:05 2007 +0200 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu Sep 27 17:55:28 2007 +0200 @@ -383,8 +383,7 @@ apply force --{* 1 subgoal left *} apply clarify -apply(drule le_imp_less_or_eq) -apply(disjE_tac) +apply(drule Nat.le_imp_less_or_eq) apply (simp_all add:Blacks_def) done