changeset 1478 | 2b8c2a7547ab |
parent 511 | b2be4790da7a |
child 12606 | cf1715a5f5ec |
1477:4c51ab632cda | 1478:2b8c2a7547ab |
---|---|
1 (* Title: ZF/IMP/Equiv.thy |
1 (* Title: ZF/IMP/Equiv.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 *) |
5 *) |
6 |
6 |
7 Equiv = Denotation + Com |
7 Equiv = Denotation + Com |