author | nipkow |
Sun, 30 Mar 1997 13:40:38 +0200 | |
changeset 2847 | 6226b83ce2d8 |
parent 2846 | 53c76f9d95fd |
child 2848 | f1cd1ad27588 |
--- 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