changeset 41589 | bbd861837ebc |
parent 34055 | fdf294ee08b2 |
child 42174 | d0be2722ce9f |
41588:9546828c0eb3 | 41589:bbd861837ebc |
---|---|
1 (* Title: HOL/IMP/Denotation.thy |
1 (* Title: HOL/IMP/Denotation.thy |
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
2 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
4 Copyright 1994 TUM |
|
5 *) |
3 *) |
6 |
4 |
7 header "Denotational Semantics of Commands" |
5 header "Denotational Semantics of Commands" |
8 |
6 |
9 theory Denotation imports Natural begin |
7 theory Denotation imports Natural begin |