| changeset 27682 | 25aceefd4786 | 
| parent 27580 | e16f4baa3db6 | 
| child 28041 | f496e9f343b7 | 
--- a/src/HOL/Library/Quicksort.thy Fri Jul 25 12:03:32 2008 +0200 +++ b/src/HOL/Library/Quicksort.thy Fri Jul 25 12:03:34 2008 +0200 @@ -18,7 +18,7 @@ by pat_completeness auto termination by (relation "measure size") - (auto simp: length_filter_le [THEN order_class.le_less_trans]) + (auto simp: length_filter_le [THEN preorder_class.le_less_trans]) lemma quicksort_permutes [simp]: "multiset_of (quicksort xs) = multiset_of xs"