| changeset 72990 | db8f94656024 |
| parent 72807 | ea189da0ff60 |
| child 74503 | 403ce50e6a2a |
--- a/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 21:32:24 2020 +0100 +++ b/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 22:25:22 2020 +0100 @@ -5,9 +5,7 @@ section \<open>Examples using Hoare Logic for Total Correctness\<close> theory ExamplesTC - -imports Hoare_Logic - + imports Hoare_Logic begin text \<open>