src/HOL/Lambda/Commutation.thy
changeset 8624 69619f870939
parent 3439 54785105178c
child 9811 39ffdb8cab03
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Mar 30 19:45:18 2000 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Mar 30 19:45:51 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Abstract commutation and confluence notions.
     1.5  *)
     1.6  
     1.7 -Commutation = Trancl +
     1.8 +Commutation = Main +
     1.9  
    1.10  consts
    1.11    square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"