src/HOL/Lambda/Commutation.thy

--- a/src/HOL/Lambda/Commutation.thy	Thu Mar 30 19:45:18 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Thu Mar 30 19:45:51 2000 +0200
@@ -6,7 +6,7 @@
 Abstract commutation and confluence notions.
 *)
 
-Commutation = Trancl +
+Commutation = Main +
 
 consts
   square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"