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.
added lemma
authornipkow
Wed, 18 Dec 2013 17:52:44 +0100
changeset 54809 319358e48bb1
parent 54802 9ce867291c76
child 54810 2392572d6c3c
added lemma
src/HOL/IMP/Hoare_Sound_Complete.thy file | annotate | diff | comparison | revisions 
--- 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 "\<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