Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Wed, 18 Dec 2013 17:52:52 +0100
changeset 54810 2392572d6c3c
parent 54808 f0fd945692bb (current diff)
parent 54809 319358e48bb1 (diff)
child 54812 a368cd086e46
merged
--- 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
isabelle