# HG changeset patch
# User nipkow
# Date 1370252257 -7200
# Node ID b7c8675437ecc489cd5143c9620d0fbe0cc49725
# Parent  9be30aa5a39b1e2ace6d16317b9f78eebc789102
corrected name

diff -r 9be30aa5a39b -r b7c8675437ec src/HOL/IMP/Hoare_Sound_Complete.thy
--- 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)