author | hoelzl |
Mon, 26 Jan 2015 14:40:13 +0100 | |
changeset 59451 | 86be42bb5174 |
parent 59450 | e82c72f3b227 |
child 59452 | 2538b2c51769 |
--- a/src/HOL/IMP/Big_Step.thy Mon Jan 26 14:34:10 2015 +0100 +++ b/src/HOL/IMP/Big_Step.thy Mon Jan 26 14:40:13 2015 +0100 @@ -6,7 +6,7 @@ text {* The big-step semantics is a straight-forward inductive definition -with concrete syntax. Note that the first paramenter is a tuple, +with concrete syntax. Note that the first parameter is a tuple, so the syntax becomes @{text "(c,s) \<Rightarrow> s'"}. *}