changeset 12036 | 49f6c49454c2 |
parent 10835 | f4745d77e620 |
child 14981 | e73f8140af78 |
12035:f2ee4b5d02f2 | 12036:49f6c49454c2 |
---|---|
1 (* Title: HOLCF/ex/Loop.thy |
1 (* Title: HOLCF/ex/Loop.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Theory for a loop primitive like while |
6 Theory for a loop primitive like while |
7 *) |
7 *) |
8 |
8 |
9 Loop = Tr + |
9 Loop = Tr + |