equal
deleted
inserted
replaced
8 |
8 |
9 Qsort = Sorting + |
9 Qsort = Sorting + |
10 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
10 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" |
11 |
11 |
12 recdef qsort "measure (size o snd)" |
12 recdef qsort "measure (size o snd)" |
13 simpset "simpset() addsimps [less_Suc_eq_le]" |
13 simpset "simpset() addsimps [length_filter RS le_less_trans]" |
14 |
14 |
15 "qsort(le, []) = []" |
15 "qsort(le, []) = []" |
16 |
16 |
17 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
17 "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) |
18 @ (x # qsort(le, [y:xs . le x y]))" |
18 @ (x # qsort(le, [y:xs . le x y]))" |