author | wenzelm |
Mon, 29 May 2006 21:09:45 +0200 | |
changeset 19749 | a49881f91cce |
parent 19748 | 5d05d091eecb |
child 19750 | 5281bd607206 |
--- 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})"