--- a/turing_basic.thy	Sun Jan 13 11:29:33 2013 +0000
+++ b/turing_basic.thy	Sun Jan 13 23:59:29 2013 +0000
@@ -621,6 +621,8 @@
   It deals with the situtation when both @{text "A"} and @{text "B"} are terminated.
 *}
 
+thm t_merge_pre_halt_same
+
 lemma t_merge_halt: 
   assumes aimpb: "Q1 \<turnstile>-> P2"
   shows "P1 \<turnstile>->  \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (A |+| B)  stp = (0, tp') \<and> Q2 tp')"