Replaced (s,t) : id by s=t.
authornipkow
Sun Mar 30 13:40:38 1997 +0200 (1997-03-30)
changeset 28476226b83ce2d8
parent 2846 53c76f9d95fd
child 2848 f1cd1ad27588
Replaced (s,t) : id by s=t.
src/HOL/IMP/Denotation.thy
     1.1 --- a/src/HOL/IMP/Denotation.thy	Thu Mar 27 17:46:24 1997 +0100
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Sun Mar 30 13:40:38 1997 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  constdefs
     1.5    Gamma :: [bexp,com_den] => (com_den => com_den)
     1.6             "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
     1.7 -                                 {(s,t). (s,t) : id & ~b(s)})"
     1.8 +                                 {(s,t). s=t & ~b(s)})"
     1.9      
    1.10  consts
    1.11    C     :: com => com_den