diff -r b9d0dd18c81e -r f2bda6ba4952 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sun Jan 27 20:01:13 2013 +0000
+++ b/thys/turing_basic.thy	Mon Jan 28 02:38:57 2013 +0000
@@ -233,6 +233,11 @@
   shows "length (A |+| B) = length A + length B"
 by auto
 
+lemma tm_comp_wf[intro]: 
+  "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
+by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
+
+
 lemma tm_comp_step: 
   assumes unfinal: "\<not> is_final (step0 c A)"
   shows "step0 c (A |+| B) = step0 c A"