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