diff -r 3d5b2b874e14 -r a73f8a7784bd ex/insort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/insort.thy	Wed Feb 23 10:05:35 1994 +0100
@@ -0,0 +1,22 @@
+(*  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"
+
+rules
+  ins_Nil  "ins(f,x,[]) = [x]"
+  ins_Cons "ins(f,x,Cons(y,ys)) =   \
+\	       if(f(x,y), Cons(x,Cons(y,ys)), Cons(y, ins(f,x,ys)))"
+
+  insort_Nil  "insort(f,[]) = []"
+  insort_Cons "insort(f,Cons(x,xs)) = ins(f,x,insort(f,xs))"
+end