# HG changeset patch
# User wenzelm
# Date 1390684700 -3600
# Node ID de95c97efab348673e0ee28d09cab10cef2e0fb5
# Parent  ee5a0ca00b6f6dce95a63b68ffe1770a5f3fb4fe# Parent  04448228381de3b493d3a47a0b57bc48d5d8fb9f
merged

diff -r 04448228381d -r de95c97efab3 src/HOL/IMP/Hoare_Total.thy
--- 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