--- a/src/HOL/IMP/Hoare_Total_EX2.thy Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare_Total_EX2.thy Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsubsection "Hoare Logic for Total Correctness With Logical Variables"
+
theory Hoare_Total_EX2
imports Hoare
begin
-subsubsection "Hoare Logic for Total Correctness --- With Logical Variables"
-
text\<open>This is the standard set of rules that you find in many publications.
In the while-rule, a logical variable is needed to remember the pre-value
of the variant (an expression that decreases by one with each iteration).