--- a/recursive.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/recursive.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -4782,7 +4782,7 @@
 done
 
 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; 
-       (a, b) \<in> set (abacus.tshift (abacus.tshift tinc_b (2 * n)) 
+       (a, b) \<in> set (tshift (tshift tinc_b (2 * n)) 
                             (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
@@ -4794,7 +4794,7 @@
   layout_of.simps length_of.simps startof_not0)
 done
 
-lemma findnth_le[elim]: "(a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))
+lemma findnth_le[elim]: "(a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))
         \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)"
 apply(induct n, simp add: findnth.simps tshift.simps)
 apply(simp add: findnth.simps tshift_append, auto)
@@ -4803,7 +4803,7 @@
 
 
 lemma  [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; (a, b) \<in> 
-  set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> 
+  set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> 
   \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
@@ -4831,7 +4831,7 @@
 
 lemma [elim]: "\<lbrakk>k < length ap; 
         ap ! k = Dec n e;
-         (a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
+         (a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> 
      start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k) \<and>
@@ -4842,7 +4842,7 @@
 done
 
 thm length_of.simps
-lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (abacus.tshift (abacus.tshift tdec_b (2 * n))
+lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (tshift (tshift tdec_b (2 * n))
                   (start_of (layout_of ap) k - Suc 0))\<rbrakk>
        \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0")