diff -r ff13585fbdab -r d8d0f8f51d69 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Sorting.thy	Sat May 27 17:42:02 2006 +0200
@@ -24,12 +24,12 @@
   "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
 
 
-constdefs
+definition
   total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
-   "total r == (\<forall>x y. r x y | r y x)"
+   "total r = (\<forall>x y. r x y | r y x)"
   
   transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
-   "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
+   "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
 
 
 
@@ -44,8 +44,8 @@
 done
 
 lemma sorted_append [simp]:
- "sorted le (xs@ys) = 
-  (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
-by (induct xs, auto)
+  "sorted le (xs@ys) = 
+    (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+  by (induct xs) auto
 
 end