src/HOL/ex/InSort.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 1896 df4e40b9ff6d
child 5184 9b8547a9496a
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/insort.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Insertion sort
     7 *)
     8 
     9 InSort  =  Sorting +
    10 
    11 consts
    12   ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
    13   insort :: [['a,'a]=>bool, 'a list] => 'a list
    14 
    15 primrec ins List.list
    16   "ins f x [] = [x]"
    17   "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
    18 primrec insort List.list
    19   "insort f [] = []"
    20   "insort f (x#xs) = ins f x (insort f xs)"
    21 end
    22