# HG changeset patch
# User nipkow
# Date 1358253979 -3600
# Node ID fb0fcd278ac5534d6510875d62201986c5063f63
# Parent  3a1edaa0dc6d9e371a2af4224ee6944a21982097
tuned

diff -r 3a1edaa0dc6d -r fb0fcd278ac5 src/HOL/IMP/Abs_Int0.thy
--- 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)"
 
diff -r 3a1edaa0dc6d -r fb0fcd278ac5 src/HOL/IMP/Abs_Int1.thy
--- 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)"