src/HOL/IMP/Abs_Int0.thy

 subsection "Computable Abstract Interpretation"
 
 text{* Abstract interpretation over type @{text st} instead of
 functions. *}
 
-context Val_abs
+context Gamma
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
 "aval' (N n) S = num' n" |
 "aval' (V x) S = lookup S x" |

 
 text{* The for-clause (here and elsewhere) only serves the purpose of fixing
 the name of the type parameter @{typ 'av} which would otherwise be renamed to
 @{typ 'a}. *}
 
-locale Abs_Int = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
+locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set"
 begin
 
 fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where
 "step' S (SKIP {P}) = (SKIP {S})" |
 "step' S (x ::= e {P}) =