update
authornipkow
Fri Oct 15 18:16:11 2004 +0200 (2004-10-15)
changeset 1524798d3ca56684d
parent 15246 0984a2c2868b
child 15248 b436486091a6
update
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/ex/Qsort.thy
     1.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Fri Oct 15 18:16:03 2004 +0200
     1.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Fri Oct 15 18:16:11 2004 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4  apply force
     1.5  apply force
     1.6  apply force
     1.7 -apply (force simp add: less_Suc_eq_le length_filter)
     1.8 +apply (force simp add: less_Suc_eq_le)
     1.9  apply force
    1.10  apply (force dest:subset_antisym)
    1.11  apply force
     2.1 --- a/src/HOL/ex/Qsort.thy	Fri Oct 15 18:16:03 2004 +0200
     2.2 +++ b/src/HOL/ex/Qsort.thy	Fri Oct 15 18:16:11 2004 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  "qsort(le, [])   = []"
     2.5  "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ [x] @
     2.6                     qsort(le, [y:xs . le x y])"
     2.7 -(hints recdef_simp: length_filter[THEN le_less_trans])
     2.8 +(hints recdef_simp: length_filter_le[THEN le_less_trans])
     2.9  
    2.10  lemma qsort_permutes[simp]:
    2.11   "multiset (qsort(le,xs)) x = multiset xs x"
    2.12 @@ -43,7 +43,7 @@
    2.13  recdef quickSort "measure size"
    2.14  "quickSort []   = []"
    2.15  "quickSort (x#l) = quickSort [y:l. ~ x<=y] @ [x] @ quickSort [y:l. x<=y]"
    2.16 -(hints recdef_simp: length_filter[THEN le_less_trans])
    2.17 +(hints recdef_simp: length_filter_le[THEN le_less_trans])
    2.18  
    2.19  lemma quickSort_permutes[simp]:
    2.20   "multiset (quickSort xs) z = multiset xs z"