--- a/thys/UTM.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/UTM.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -1439,7 +1439,7 @@
 apply(simp add: t_twice_def t_twice_compile_def)
 using mopup_mod2[of 1]
 apply(simp)
-by arith
+done
 
 lemma wcode_jump1: 
   "\<exists> stp ln rn. steps0 (Suc (t_twice_len) + length t_wcode_main_first_part div 2,
@@ -2069,7 +2069,7 @@
 
 lemma [intro]: "length t_twice mod 2 = 0"
 apply(auto simp: t_twice_def t_twice_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma t_fourtimes_append_pre:
   "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp
@@ -2131,11 +2131,11 @@
 
 lemma even_twice_len: "length t_twice mod 2 = 0"
 apply(auto simp: t_twice_def t_twice_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0"
 apply(auto simp: t_fourtimes_def t_fourtimes_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma [simp]: "2 * (length t_twice div 2) = length t_twice"
 using even_twice_len