--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Oct 15 18:16:03 2004 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Fri Oct 15 18:16:11 2004 +0200
@@ -511,7 +511,7 @@
apply force
apply force
apply force
-apply (force simp add: less_Suc_eq_le length_filter)
+apply (force simp add: less_Suc_eq_le)
apply force
apply (force dest:subset_antisym)
apply force
--- a/src/HOL/ex/Qsort.thy Fri Oct 15 18:16:03 2004 +0200
+++ b/src/HOL/ex/Qsort.thy Fri Oct 15 18:16:11 2004 +0200
@@ -15,7 +15,7 @@
"qsort(le, []) = []"
"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
qsort(le, [y:xs . le x y])"
-(hints recdef_simp: length_filter[THEN le_less_trans])
+(hints recdef_simp: length_filter_le[THEN le_less_trans])
lemma qsort_permutes[simp]:
"multiset (qsort(le,xs)) x = multiset xs x"
@@ -43,7 +43,7 @@
recdef quickSort "measure size"
"quickSort [] = []"
"quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
-(hints recdef_simp: length_filter[THEN le_less_trans])
+(hints recdef_simp: length_filter_le[THEN le_less_trans])
lemma quickSort_permutes[simp]:
"multiset (quickSort xs) z = multiset xs z"