equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsection "Annotated Commands" |
2 |
4 |
3 theory ACom |
5 theory ACom |
4 imports Com |
6 imports Com |
5 begin |
7 begin |
6 |
|
7 subsection "Annotated Commands" |
|
8 |
8 |
9 datatype 'a acom = |
9 datatype 'a acom = |
10 SKIP 'a ("SKIP {_}" 61) | |
10 SKIP 'a ("SKIP {_}" 61) | |
11 Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
11 Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
12 Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | |
12 Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | |