diff -r f04b33ce250f -r a4dc62a46ee4 ex/InSort.thy
--- 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