--- a/thys/abacus.thy	Sun Feb 03 12:24:28 2013 +0000
+++ b/thys/abacus.thy	Sun Feb 03 13:31:14 2013 +0000
@@ -3,9 +3,19 @@
 *}
 
 theory abacus
-imports Main turing_basic
+imports uncomputable
 begin
 
+(*
+declare tm_comp.simps [simp add] 
+declare adjust.simps[simp add] 
+declare shift.simps[simp add]
+declare tm_wf.simps[simp add]
+declare step.simps[simp add]
+declare steps.simps[simp add]
+*)
+declare replicate_Suc[simp add]
+
 text {*
   {\em Abacus} instructions:
 *}
@@ -1300,8 +1310,7 @@
    inv_locate_b.simps[simp del]
 
 lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
-apply(rule_tac x = "Suc 0" in exI, simp)
-done
+by (metis replicate_0 replicate_Suc)
 
 lemma [intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
              \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires"
@@ -1877,7 +1886,6 @@
      \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires"
 apply(auto simp: inv_on_right_moving.simps inv_after_write.simps )
 apply(case_tac mr, auto simp: split: if_splits)
-apply(case_tac [!] mr, simp_all)
 done
       
 lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow>