--- a/thys/turing_hoare.thy	Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/turing_hoare.thy	Wed Jan 23 08:01:35 2013 +0100
@@ -53,17 +53,17 @@
 
 
 text {*
-  {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2   A, B well-formed
-  ------------------------------------------------------
+  {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2   A well-formed
+  ---------------------------------------------------
   {P1} A |+| B {Q2}
 *}
 
 
 lemma Hoare_plus_halt: 
-  assumes a_imp: "Q1 \<mapsto> P2"
+  assumes A_halt : "{P1} A {Q1}"
+  and B_halt : "{P2} B {Q2}"
+  and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
-  and A_halt : "{P1} A {Q1}"
-  and B_halt : "{P2} B {Q2}"
   shows "{P1} A |+| B {Q2}"
 proof(rule HoareI)
   fix l r
@@ -103,10 +103,10 @@
 
 
 lemma Hoare_plus_unhalt:
-  assumes a_imp: "Q1 \<mapsto> P2"
+  assumes A_halt: "{P1} A {Q1}"
+  and B_uhalt: "{P2} B \<up>"
+  and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
-  and A_halt : "{P1} A {Q1}"
-  and B_uhalt : "{P2} B \<up>"
   shows "{P1} (A |+| B) \<up>"
 proof(rule_tac Hoare_unhalt_I)
   fix n l r 
@@ -155,13 +155,5 @@
 by (metis holds_for.simps surj_pair)
 
 
-declare tm_comp.simps [simp del] 
-declare adjust.simps[simp del] 
-declare shift.simps[simp del]
-declare tm_wf.simps[simp del]
-declare step.simps[simp del]
-declare steps.simps[simp del]
-
-
 
 end
\ No newline at end of file