author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5184 | 9b8547a9496a |
child 8422 | 6c6a5410a9bd |
permissions | -rw-r--r-- |
(* Title: HOL/ex/insort.thy ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen Insertion sort *) InSort = Sorting + consts ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list insort :: [['a,'a]=>bool, 'a list] => 'a list primrec "ins f x [] = [x]" "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" primrec "insort f [] = []" "insort f (x#xs) = ins f x (insort f xs)" end