changeset 8524 | f990040535c9 |
parent 8414 | 5983668cac15 |
child 8590 | 89675b444abe |
--- a/src/HOL/ex/Qsort.thy Mon Mar 20 10:24:07 2000 +0100 +++ b/src/HOL/ex/Qsort.thy Mon Mar 20 10:26:34 2000 +0100 @@ -10,7 +10,7 @@ consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" recdef qsort "measure (size o snd)" - simpset "simpset() addsimps [less_Suc_eq_le]" + simpset "simpset() addsimps [length_filter RS le_less_trans]" "qsort(le, []) = []"