equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close> |
7 section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close> |
8 |
8 |
9 theory Hoare_Logic_Abort |
9 theory Hoare_Logic_Abort |
10 imports Hoare_Syntax Hoare_Tac |
10 imports Hoare_Syntax Hoare_Tac |
11 begin |
11 begin |
12 |
12 |
13 type_synonym 'a bexp = "'a set" |
13 type_synonym 'a bexp = "'a set" |
14 type_synonym 'a assn = "'a set" |
14 type_synonym 'a assn = "'a set" |
15 type_synonym 'a var = "'a \<Rightarrow> nat" |
15 type_synonym 'a var = "'a \<Rightarrow> nat" |