# HG changeset patch # User nipkow # Date 1387385564 -3600 # Node ID 319358e48bb12a4b66f875f80d08aa0e12a4f534 # Parent 9ce867291c76330f48759402265375520e941544 added lemma diff -r 9ce867291c76 -r 319358e48bb1 src/HOL/IMP/Hoare_Sound_Complete.thy --- a/src/HOL/IMP/Hoare_Sound_Complete.thy Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Wed Dec 18 17:52:44 2013 +0100 @@ -77,4 +77,7 @@ show "\ {wp c Q} c {Q}" by(rule wp_is_pre) qed +corollary hoare_sound_complete: "\ {P}c{Q} \ \ {P}c{Q}" +by (metis hoare_complete hoare_sound) + end