| changeset 35762 | af3ff2ba4c54 |
| parent 21404 | eb85850d3eb7 |
| child 40945 | b8703f63bfb2 |
| 35761:c4a698ee83b4 | 35762:af3ff2ba4c54 |
|---|---|
1 (* Title: ZF/IMP/Denotation.thy |
1 (* Title: ZF/IMP/Denotation.thy |
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer and Robert Sandner, TU München |
2 Author: Heiko Loetzbeyer and Robert Sandner, TU München |
4 *) |
3 *) |
5 |
4 |
6 header {* Denotational semantics of expressions and commands *} |
5 header {* Denotational semantics of expressions and commands *} |
7 |
6 |