# HG changeset patch
# User nipkow
# Date 859722038 -7200
# Node ID 6226b83ce2d85dd0865085419e61a9ab3645da79
# Parent  53c76f9d95fdb79a48609b6abc418edabf05fa43
Replaced (s,t) : id by s=t.

diff -r 53c76f9d95fd -r 6226b83ce2d8 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Thu Mar 27 17:46:24 1997 +0100
+++ b/src/HOL/IMP/Denotation.thy	Sun Mar 30 13:40:38 1997 +0200
@@ -13,7 +13,7 @@
 constdefs
   Gamma :: [bexp,com_den] => (com_den => com_den)
            "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
-                                 {(s,t). (s,t) : id & ~b(s)})"
+                                 {(s,t). s=t & ~b(s)})"
     
 consts
   C     :: com => com_den