--- a/thys/turing_basic.thy	Wed Jan 16 15:17:02 2013 +0000
+++ b/thys/turing_basic.thy	Thu Jan 17 11:51:00 2013 +0000
@@ -93,7 +93,6 @@
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2
                                              + off \<and> s \<ge> off))"
 
-
 (* FIXME: needed? *)
 lemma halt_lemma: 
   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
@@ -102,6 +101,18 @@
 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)
   where "x \<up> n == replicate n x"
 
+consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)
+
+fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" 
+  where 
+  "tape_of_nat_list [] = []" |
+  "tape_of_nat_list [n] = Oc\<up>(Suc n)" |
+  "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"
+
+defs (overloaded)
+  tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am"
+  tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
+
 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool"
   where
   "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"
@@ -598,8 +609,6 @@
       done
   qed
 qed
-    
-      
-       
+        
 end