--- a/thys/UF.thy	Thu May 02 13:19:50 2013 +0100
+++ b/thys/UF.thy	Thu May 09 18:16:36 2013 +0100
@@ -3752,10 +3752,10 @@
 done
 
 lemma [simp]: "left (trpl l st r) = l"
-apply(simp add: left.simps trpl.simps lo.simps 
-              loR.simps mod_dvd_simp, auto simp: conf_decode1)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",
-      auto)
+apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp)
+apply(auto simp: conf_decode1)
+apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r")
+apply(auto)
 apply(erule_tac x = l in allE, auto)
 done   
 
@@ -4613,6 +4613,7 @@
   "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); 
     tm_wf (tp,0); 0<rs\<rbrakk>
    \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+thm halt_least_step nonstop_t_eq nonstop_lemma rec_t_eq_steps conf_lemma
 apply(frule_tac halt_least_step, auto)
 apply(frule_tac  nonstop_t_eq, auto simp: nonstop_lemma)
 using rec_t_eq_steps[of tp l lm stp]