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