src/HOL/ex/InSort.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8422 6c6a5410a9bd
child 13159 2af7b94892ce
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  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 le x [] = [x]"
  "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"
primrec
  "insort le [] = []"
  "insort le (x#xs) = ins le x (insort le xs)"
end