changeset 16417 | 9bc16273c2d4 |
parent 13020 | 791e3b4c4039 |
child 23746 | a455e69c31cc |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 |
1 |
2 header {* \section{Operational Semantics} *} |
2 header {* \section{Operational Semantics} *} |
3 |
3 |
4 theory OG_Tran = OG_Com: |
4 theory OG_Tran imports OG_Com begin |
5 |
5 |
6 types |
6 types |
7 'a ann_com_op = "('a ann_com) option" |
7 'a ann_com_op = "('a ann_com) option" |
8 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)" |
8 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)" |
9 |
9 |