--- a/src/HOL/IMP/Hoare_Total_EX.thy Fri Jul 22 17:35:54 2016 +0200
+++ b/src/HOL/IMP/Hoare_Total_EX.thy Sat Jul 23 13:25:44 2016 +0200
@@ -1,8 +1,10 @@
(* Author: Tobias Nipkow *)
-theory Hoare_Total_EX imports Hoare_Sound_Complete Hoare_Examples begin
+theory Hoare_Total_EX
+imports Hoare
+begin
-subsection "Hoare Logic for Total Correctness"
+subsubsection "Hoare Logic for Total Correctness --- \<open>nat\<close>-Indexed Invariant"
text{* This is the standard set of rules that you find in many publications.
The While-rule is different from the one in Concrete Semantics in that the