| changeset 16417 | 9bc16273c2d4 |
| parent 13020 | 791e3b4c4039 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 |
1 |
2 header {* \chapter{The Owicki-Gries Method} |
2 header {* \chapter{The Owicki-Gries Method} |
3 |
3 |
4 \section{Abstract Syntax} *} |
4 \section{Abstract Syntax} *} |
5 |
5 |
6 theory OG_Com = Main: |
6 theory OG_Com imports Main begin |
7 |
7 |
8 text {* Type abbreviations for boolean expressions and assertions: *} |
8 text {* Type abbreviations for boolean expressions and assertions: *} |
9 |
9 |
10 types |
10 types |
11 'a bexp = "'a set" |
11 'a bexp = "'a set" |