# HG changeset patch
# User nipkow
# Date 1097856971 -7200
# Node ID 98d3ca56684d49d878734eaaa76dc8667fc68fe3
# Parent  0984a2c2868bccd117e0eb8e6fd7e2852ed42994
update

diff -r 0984a2c2868b -r 98d3ca56684d src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- 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
diff -r 0984a2c2868b -r 98d3ca56684d src/HOL/ex/Qsort.thy
--- 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"