# HG changeset patch
# User nipkow
# Date 1387385572 -3600
# Node ID 2392572d6c3cb7bb60b939b8439ec463ea13cbdc
# Parent  f0fd945692bbdf9066f8f19ef698e9a7a080573e# Parent  319358e48bb12a4b66f875f80d08aa0e12a4f534
merged

diff -r f0fd945692bb -r 2392572d6c3c src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Dec 18 17:48:48 2013 +0100
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Dec 18 17:52:52 2013 +0100
@@ -77,4 +77,7 @@
   show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
 qed
 
+corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
+by (metis hoare_complete hoare_sound)
+
 end