| changeset 1376 | 92f83b9d17e1 |
| parent 969 | b051e2fc2e34 |
| child 1476 | 608483c2122a |
--- a/src/HOL/ex/InSort.thy Thu Nov 30 12:58:44 1995 +0100 +++ b/src/HOL/ex/InSort.thy Fri Dec 01 12:03:13 1995 +0100 @@ -9,8 +9,8 @@ InSort = Sorting + consts - ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" - insort :: "[['a,'a]=>bool, 'a list] => 'a list" + 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]"