fixed auto steps (due to changed atomize);

--- 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 

--- a/src/HOL/Unix/Unix.thy	Sun Oct 14 20:06:13 2001 +0200
+++ b/src/HOL/Unix/Unix.thy	Sun Oct 14 20:07:11 2001 +0200
@@ -696,7 +696,7 @@
           xs_y: "r =(xs @ [y])\<Rightarrow> root''"
         by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
       from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
-        by (auto simp add: can_exec_def)
+        by (unfold can_exec_def) blast
       from x xs have "root =(x # xs)\<Rightarrow> root'"
         by (rule transitions.cons)
       with y show ?thesis by blast