src/HOL/IMP/Abs_Int1.thy

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

 by(simp add: \<gamma>_st_def)
 
 end
 
 
-locale Abs_Int = Gamma where \<gamma>=\<gamma>
+locale Abs_Int = Gamma_semilattice where \<gamma>=\<gamma>
   for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
 begin
 
 definition "step' = Step
   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))