changeset 50896 | fb0fcd278ac5 |
parent 49547 | 78be750222cf |
child 50986 | c54ea7f5418f |
--- a/src/HOL/IMP/Abs_Int1.thy Mon Jan 14 23:08:40 2013 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Tue Jan 15 13:46:19 2013 +0100 @@ -44,7 +44,7 @@ begin fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where -"aval' (N n) S = num' n" | +"aval' (N i) S = num' i" | "aval' (V x) S = fun S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"