--- a/src/HOL/CTL/CTL.thy Sun Oct 14 20:06:13 2001 +0200
+++ b/src/HOL/CTL/CTL.thy Sun Oct 14 20:07:11 2001 +0200
@@ -292,8 +292,8 @@
proof
have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
- also note Int_mono AG_mono
- ultimately show "?lhs \<subseteq> \<AG> p" by auto
+ also note Int_mono AG_mono
+ ultimately show "?lhs \<subseteq> \<AG> p" by fast
next
have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
moreover