changeset 68776 | 403dd13cf6e9 |
parent 67443 | 3abf6a722518 |
child 69505 | cc2d676d5395 |
--- a/src/HOL/IMP/Big_Step.thy Fri Aug 17 11:26:35 2018 +0000 +++ b/src/HOL/IMP/Big_Step.thy Mon Aug 20 20:54:26 2018 +0200 @@ -1,9 +1,9 @@ (* Author: Gerwin Klein, Tobias Nipkow *) +subsection "Big-Step Semantics of Commands" + theory Big_Step imports Com begin -subsection "Big-Step Semantics of Commands" - text \<open> The big-step semantics is a straight-forward inductive definition with concrete syntax. Note that the first parameter is a tuple,