diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -25,10 +25,11 @@
 
 
 definition
-  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
+  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
    "total r = (\<forall>x y. r x y | r y x)"
   
-  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
+definition
+  transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
    "transf f = (\<forall>x y z. f x y & f y z --> f x z)"