1.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Dec 18 17:48:48 2013 +0100
     1.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Wed Dec 18 17:52:52 2013 +0100
     1.3 @@ -77,4 +77,7 @@
     1.4    show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
     1.5  qed
     1.6  
     1.7 +corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
     1.8 +by (metis hoare_complete hoare_sound)
     1.9 +
    1.10  end