| changeset 54252 | a4a00347e59f |
| parent 53015 | a1119cf551e8 |
| child 54289 | 5a1be63f32cf |
--- a/src/HOL/IMP/AExp.thy Mon Nov 04 20:10:10 2013 +0100 +++ b/src/HOL/IMP/AExp.thy Tue Nov 05 15:30:53 2013 +1100 @@ -37,7 +37,7 @@ text {* \noindent We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: *} -lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)" +lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" by (rule refl) value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"