| changeset 67019 | 7a3724078363 |
| parent 63538 | d7b5e2a222c2 |
| child 67406 | 23307fd33906 |
--- a/src/HOL/IMP/VCG_Total_EX.thy Tue Nov 07 11:11:37 2017 +0100 +++ b/src/HOL/IMP/VCG_Total_EX.thy Tue Nov 07 14:52:27 2017 +0100 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) theory VCG_Total_EX -imports "~~/src/HOL/IMP/Hoare_Total_EX" +imports Hoare_Total_EX begin subsection "Verification Conditions for Total Correctness"