equal
deleted
inserted
replaced
1 header "IMP --- A Simple Imperative Language" |
1 header "IMP --- A Simple Imperative Language" |
2 |
2 |
3 theory Com imports BExp begin |
3 theory Com imports BExp begin |
4 |
4 |
|
5 text_raw{*\begin{isaverbatimwrite}\newcommand{\Comdef}{% *} |
5 datatype |
6 datatype |
6 com = SKIP |
7 com = SKIP |
7 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
8 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
8 | Semi com com ("_;/ _" [60, 61] 60) |
9 | Semi com com ("_;/ _" [60, 61] 60) |
9 | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
10 | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
10 | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) |
11 | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) |
|
12 text_raw{*}\end{isaverbatimwrite}*} |
11 |
13 |
12 end |
14 end |