merged

--- a/src/HOL/IMP/Hoare_Total.thy	Sat Jan 25 22:06:07 2014 +0100
+++ b/src/HOL/IMP/Hoare_Total.thy	Sat Jan 25 22:18:20 2014 +0100
@@ -209,4 +209,7 @@
 apply(auto simp: hoare_tvalid_def wpt_def)
 done
 
+corollary hoaret_sound_complete: "\<turnstile>\<^sub>t {P}c{Q} \<longleftrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
+by (metis hoaret_sound hoaret_complete)
+
 end