1.1 --- a/src/ZF/IMP/Denotation.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/ZF/IMP/Denotation.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    C     :: "i => i"
     1.5  
     1.6  definition
     1.7 -  Gamma :: "[i,i,i] => i"    ("\<Gamma>")
     1.8 +  Gamma :: "[i,i,i] => i"  ("\<Gamma>") where
     1.9    "\<Gamma>(b,cden) ==
    1.10      (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>
    1.11             {io \<in> id(loc->nat). B(b,fst(io))=0})"