equal
deleted
inserted
replaced
1 |
1 |
2 header {* \section{Operational Semantics} *} |
2 header {* \section{Operational Semantics} *} |
3 |
3 |
4 theory OG_Tran imports OG_Com begin |
4 theory OG_Tran imports OG_Com begin |
5 |
5 |
6 types |
6 type_synonym 'a ann_com_op = "('a ann_com) option" |
7 'a ann_com_op = "('a ann_com) option" |
7 type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)" |
8 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)" |
|
9 |
8 |
10 primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where |
9 primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where |
11 "com (c, q) = c" |
10 "com (c, q) = c" |
12 |
11 |
13 primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where |
12 primrec post :: "'a ann_triple_op \<Rightarrow> 'a assn" where |