src/ZF/IMP/Denotation.thy

--- a/src/ZF/IMP/Denotation.thy	Mon May 29 17:38:30 2006 +0200
+++ b/src/ZF/IMP/Denotation.thy	Mon May 29 19:23:04 2006 +0200
@@ -14,9 +14,9 @@
   B     :: "i => i => i"
   C     :: "i => i"
 
-constdefs
+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})"