# HG changeset patch
# User nipkow
# Date 1390673227 -3600
# Node ID ee5a0ca00b6f6dce95a63b68ffe1770a5f3fb4fe
# Parent  9808f186795ce5bc695c3979cb73002557830eb3
added lemma

diff -r 9808f186795c -r ee5a0ca00b6f src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Fri Jan 24 16:54:25 2014 +0000
+++ b/src/HOL/IMP/Hoare_Total.thy	Sat Jan 25 19:07:07 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