| changeset 58884 | be4d203d35b3 |
| parent 46362 | b2878f059f91 |
| child 59189 | ad8e0a789af6 |
| 58883:fef1df4268d6 | 58884:be4d203d35b3 |
|---|---|
1 |
1 section {* The Proof System *} |
2 header {* \section{The Proof System} *} |
|
3 |
2 |
4 theory OG_Hoare imports OG_Tran begin |
3 theory OG_Hoare imports OG_Tran begin |
5 |
4 |
6 primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where |
5 primrec assertions :: "'a ann_com \<Rightarrow> ('a assn) set" where |
7 "assertions (AnnBasic r f) = {r}" |
6 "assertions (AnnBasic r f) = {r}" |