--- a/src/HOL/IMP/HoareT.thy Wed Sep 28 10:35:56 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy Thu Sep 29 21:42:03 2011 +0200
@@ -10,7 +10,7 @@
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
"\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)"
-text{* Proveability of Hoare triples in the proof system for total
+text{* Provability of Hoare triples in the proof system for total
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for
@{text"\<turnstile>"} only in the one place where nontermination can arise: the