equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 InSort = Sorting + |
9 InSort = Sorting + |
10 |
10 |
11 consts |
11 consts |
12 ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" |
12 ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list |
13 insort :: "[['a,'a]=>bool, 'a list] => 'a list" |
13 insort :: [['a,'a]=>bool, 'a list] => 'a list |
14 |
14 |
15 primrec ins List.list |
15 primrec ins List.list |
16 ins_Nil "ins f x [] = [x]" |
16 ins_Nil "ins f x [] = [x]" |
17 ins_Cons "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" |
17 ins_Cons "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" |
18 primrec insort List.list |
18 primrec insort List.list |