src/HOL/ex/InSort.thy
changeset 1376 92f83b9d17e1
parent 969 b051e2fc2e34
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/InSort.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/InSort.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  InSort  =  Sorting +
     1.5  
     1.6  consts
     1.7 -  ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list"
     1.8 -  insort :: "[['a,'a]=>bool, 'a list] => 'a list"
     1.9 +  ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
    1.10 +  insort :: [['a,'a]=>bool, 'a list] => 'a list
    1.11  
    1.12  primrec ins List.list
    1.13    ins_Nil  "ins f x [] = [x]"