src/CCL/Trancl.thy

--- a/src/CCL/Trancl.thy	Mon Oct 04 18:02:04 2021 +0200
+++ b/src/CCL/Trancl.thy	Mon Oct 04 18:12:55 2021 +0200
@@ -66,7 +66,6 @@
 
 lemmas [intro] = compI idI
   and [elim] = compE idE
-  and [elim!] = pair_inject
 
 lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)"
   by blast
@@ -202,8 +201,6 @@
   done
 
 lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
-  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
-   apply assumption+
-  done
+  by (rule r_into_trancl [THEN trans_trancl [THEN transD]])
 
 end