src/HOL/IMP/HoareT.thy

 header{* Hoare Logic for Total Correctness *}
 
-theory HoareT imports Hoare_Sound_Complete Util begin
+theory HoareT imports Hoare_Sound_Complete begin
 
 text{*
 Now that we have termination, we can define
 total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*}