use int example like in the rest of IMP (instead of nat)
authorkleing
Tue Nov 05 15:30:53 2013 +1100 (2013-11-05)
changeset 54252a4a00347e59f
parent 54251 adea9f6986b2
child 54253 04cd231e2b9e
use int example like in the rest of IMP (instead of nat)
src/HOL/IMP/AExp.thy
     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>"