author | kleing |
Tue, 05 Nov 2013 15:30:53 +1100 | |
changeset 55704 | a4a00347e59f |
parent 55703 | adea9f6986b2 |
child 55705 | 04cd231e2b9e |
1.1 --- a/src/HOL/IMP/AExp.thy Mon Nov 04 20:10:10 2013 +0100 1.2 +++ b/src/HOL/IMP/AExp.thy Tue Nov 05 15:30:53 2013 +1100 1.3 @@ -37,7 +37,7 @@ 1.4 text {* \noindent 1.5 We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: 1.6 *} 1.7 -lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)" 1.8 +lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" 1.9 by (rule refl) 1.10 1.11 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"