changeset 72990 | db8f94656024 |
parent 72987 | b1be35908165 |
child 73655 | 26a1d66b9077 |
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 21:32:24 2020 +0100 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 22:25:22 2020 +0100 @@ -7,7 +7,7 @@ section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close> theory Hoare_Logic_Abort -imports Hoare_Syntax Hoare_Tac + imports Hoare_Syntax Hoare_Tac begin type_synonym 'a bexp = "'a set"