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)