author | kleing |
Tue, 05 Nov 2013 15:30:53 +1100 | |
changeset 54252 | a4a00347e59f |
parent 54251 | adea9f6986b2 |
child 54253 | 04cd231e2b9e |
--- 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>"