author | nipkow |
Mon, 03 Jun 2013 11:37:37 +0200 | |
changeset 52291 | b7c8675437ec |
parent 52290 | 9be30aa5a39b |
child 52292 | 5ef34e96e14a |
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Mon Jun 03 06:41:07 2013 +0200 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Mon Jun 03 11:37:37 2013 +0200 @@ -84,7 +84,7 @@ qed qed auto -lemma hoare_relative_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" +lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}" proof(rule strengthen_pre) show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms by (auto simp: hoare_valid_def wp_def)