src/ZF/IMP/Denotation.thy

--- a/src/ZF/IMP/Denotation.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/ZF/IMP/Denotation.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -15,7 +15,7 @@
   C     :: "i => i"
 
 definition
-  Gamma :: "[i,i,i] => i"    ("\<Gamma>")
+  Gamma :: "[i,i,i] => i"  ("\<Gamma>") where
   "\<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})"