diff -r 8dc659af1bd2 -r 4c8325c64dab thys/turing_basic.thy
--- a/thys/turing_basic.thy	Fri Jan 25 22:12:01 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 26 01:36:48 2013 +0000
@@ -194,13 +194,15 @@
   "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)"
+fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" 
+  where 
+  "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" 
+
 
-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)"
+defs (overloaded)
+  tape_of_nl_abv: "<ns> \<equiv> tape_of_nat_list ns"
+  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc\<up>(Suc n)"
+  tape_of_nat_pair: "<p> \<equiv> tape_of_nat_pair p"
 
 fun 
   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"