diff -r e7d845acb0a7 -r cd4ef33c8fb1 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Sat Jan 19 14:29:56 2013 +0000
+++ b/thys/uncomputable.thy	Sat Jan 19 14:44:07 2013 +0000
@@ -6,7 +6,7 @@
 header {* Undeciablity of the {\em Halting problem} *}
 
 theory uncomputable
-imports Main turing_basic
+imports Main turing_hoare
 begin
 
 text {*
@@ -1143,15 +1143,6 @@
 apply(drule_tac length_eq, simp)
 done
 
-lemma Hoare_weak:
-  fixes p::tprog0
-  assumes a: "{P} p {Q}"
-  and b: "P' \<mapsto> P" 
-  and c: "Q \<mapsto> Q'"
-  shows "{P'} p {Q'}"
-using assms
-unfolding Hoare_def assert_imp_def
-by (blast intro: holds_for_imp[simplified assert_imp_def])
 
 text {*
   The following locale specifies that TM @{text "H"} can be used to solve