| changeset 43158 | 686fa0a0696e |
| parent 43141 | 11fce8564415 |
| child 44036 | d03f9f28d01d |
--- a/src/HOL/IMP/Small_Step.thy Mon Jun 06 16:29:13 2011 +0200 +++ b/src/HOL/IMP/Small_Step.thy Mon Jun 06 16:29:38 2011 +0200 @@ -27,7 +27,7 @@ values "{(c',map t [''x'',''y'',''z'']) |c' t. (''x'' ::= V ''z''; ''y'' ::= V ''x'', - lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}" + [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 7, ''z'' \<rightarrow> 5]) \<rightarrow>* (c',t)}" subsection{* Proof infrastructure *}