diff -r bd320b5365e2 -r d6f04e3e9894 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/thys/turing_basic.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -179,30 +179,28 @@
 abbreviation
   "tm_wf0 p \<equiv> tm_wf (p, 0)"
 
-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)"
-by (metis wf_iff_no_infinite_down_chain)
-
 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" 
+defs (overloaded)
+  tape_of_nat_abv: "<(n::nat)> \<equiv> Oc \<up> (Suc n)"
+
+fun tape_of_nat_list :: "'a 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)"
+  "tape_of_nat_list [n] = <n>" |
+  "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)"
 
-fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" 
+fun tape_of_nat_pair :: "'a \<times> 'b \<Rightarrow> cell list" 
   where 
-  "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" 
+  "tape_of_nat_pair (n, m) = <n> @ [Bk] @ <m>" 
 
 
 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"
+  tape_of_nl_abv: "<(ns::'a list)> \<equiv> tape_of_nat_list ns"
+  tape_of_nat_pair: "<(np::'a\<times>'b)> \<equiv> tape_of_nat_pair np"
 
 fun 
   shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"