--- a/thys/turing_basic.thy	Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/turing_basic.thy	Wed Jan 23 08:01:35 2013 +0100
@@ -174,6 +174,10 @@
   "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
 
+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)