src/ZF/IMP/Denotation.thy
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})"