src/ZF/ex/Commutation.thy

--- a/src/ZF/ex/Commutation.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/ex/Commutation.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -94,8 +94,8 @@
 done
 
 lemma confluent_Un: 
- "[| confluent(r); confluent(s); commute(r^*, s^*);  
-     r \<subseteq> Sigma(A,B); s \<subseteq> Sigma(C,D) |] ==> confluent(r Un s)"
+ "[| confluent(r); confluent(s); commute(r^*, s^*); 
+     relation(r); relation(s) |] ==> confluent(r Un s)"
 apply (unfold confluent_def)
 apply (rule rtrancl_Un_rtrancl [THEN subst])
 apply auto