--- a/src/HOL/IMP/Abs_Int0.thy Mon Jan 14 23:08:40 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Tue Jan 15 13:46:19 2013 +0100
@@ -242,9 +242,9 @@
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
- assumes gamma_num': "n : \<gamma>(num' n)"
+ assumes gamma_num': "i : \<gamma>(num' i)"
and gamma_plus':
- "n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)"
+ "i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma>(plus' a1 a2)"
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
@@ -252,7 +252,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 = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
--- 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)"