--- a/ex/InSort.thy Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* 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 List.list
- ins_Nil "ins(f,x,[]) = [x]"
- ins_Cons "ins(f,x,y#ys) = if(f(x,y), x#y#ys, y#ins(f,x,ys))"
-primrec insort List.list
- insort_Nil "insort(f,[]) = []"
- insort_Cons "insort(f,x#xs) = ins(f,x,insort(f,xs))"
-end