--- a/src/HOL/ex/Sorting.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/ex/Sorting.thy Fri Dec 01 12:03:13 1995 +0100
@@ -8,11 +8,11 @@
Sorting = List +
consts
- sorted1:: "[['a,'a] => bool, 'a list] => bool"
- sorted :: "[['a,'a] => bool, 'a list] => bool"
- mset :: "'a list => ('a => nat)"
- total :: "(['a,'a] => bool) => bool"
- transf :: "(['a,'a] => bool) => bool"
+ sorted1:: [['a,'a] => bool, 'a list] => bool
+ sorted :: [['a,'a] => bool, 'a list] => bool
+ mset :: 'a list => ('a => nat)
+ total :: (['a,'a] => bool) => bool
+ transf :: (['a,'a] => bool) => bool
rules