# HG changeset patch
# User wenzelm
# Date 1148929785 -7200
# Node ID a49881f91cce2e2d15fc4e32b319754c6d758a00
# Parent  5d05d091eecbe66273ac9fa8c5b8973747fafc62
proper meta definition;

diff -r 5d05d091eecb -r a49881f91cce src/ZF/IMP/Denotation.thy
--- 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})"