--- a/thys/uncomputable.thy	Sun Jan 20 16:01:16 2013 +0000
+++ b/thys/uncomputable.thy	Tue Jan 22 14:38:56 2013 +0000
@@ -996,8 +996,6 @@
 next
   show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto
 next
-  show "tm_wf (tcopy_end, 0)" by auto
-next
   assume "0 < x"
   thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}"
   proof(rule_tac Hoare_plus_halt)
@@ -1008,8 +1006,6 @@
   next
     show "tm_wf (tcopy_init, 0)" by auto
   next
-    show "tm_wf (tcopy_loop, 0)" by auto
-  next
     assume "0 < x"
     thus "{inv_init1 x} tcopy_init {inv_init0 x}"
       by(erule_tac init_correct)
@@ -1345,7 +1341,7 @@
   let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
   let ?P3 = ?Q2
   assume h: "haltP (?tcontr, 0) [code ?tcontr]"
-  have "{?P1} ?tcontr"
+  have "{?P1} ?tcontr \<up>"
   proof(rule_tac Hoare_plus_unhalt, auto)
     show "?Q2 \<mapsto> ?P3"
       apply(simp add: assert_imp_def)
@@ -1384,7 +1380,7 @@
         done
     qed
   next
-    show "{?P3} dither"
+    show "{?P3} dither \<up>"
       using Hoare_unhalt_def
     proof(auto)
       fix nd n