changeset 19749 | a49881f91cce |
parent 19747 | 163f1ba9225a |
child 21404 | eb85850d3eb7 |
--- a/src/ZF/IMP/Denotation.thy Mon May 29 19:42:58 2006 +0200 +++ b/src/ZF/IMP/Denotation.thy Mon May 29 21:09:45 2006 +0200 @@ -16,7 +16,7 @@ definition Gamma :: "[i,i,i] => i" ("\<Gamma>") - "\<Gamma>(b,cden) = + "\<Gamma>(b,cden) == (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union> {io \<in> id(loc->nat). B(b,fst(io))=0})"