# HG changeset patch
# User kleing
# Date 1383625853 -39600
# Node ID a4a00347e59fd27bcd0c303d30c940e84e910c32
# Parent  adea9f6986b2ebb6652994fc6c91d37127e8b594
use int example like in the rest of IMP (instead of nat)

diff -r adea9f6986b2 -r a4a00347e59f src/HOL/IMP/AExp.thy
--- 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>"