equal
deleted
inserted
replaced
4 |
4 |
5 subsection "Big-Step Semantics of Commands" |
5 subsection "Big-Step Semantics of Commands" |
6 |
6 |
7 text {* |
7 text {* |
8 The big-step semantics is a straight-forward inductive definition |
8 The big-step semantics is a straight-forward inductive definition |
9 with concrete syntax. Note that the first paramenter is a tuple, |
9 with concrete syntax. Note that the first parameter is a tuple, |
10 so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}. |
10 so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}. |
11 *} |
11 *} |
12 |
12 |
13 text_raw{*\snip{BigStepdef}{0}{1}{% *} |
13 text_raw{*\snip{BigStepdef}{0}{1}{% *} |
14 inductive |
14 inductive |