changeset 12036 | 49f6c49454c2 |
parent 10835 | f4745d77e620 |
child 14981 | e73f8140af78 |
12035:f2ee4b5d02f2 | 12036:49f6c49454c2 |
---|---|
1 (* Title: HOLCF/ex/hoare.thy |
1 (* Title: HOLCF/ex/hoare.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 an example by C.A.R. Hoare |
6 Theory for an example by C.A.R. Hoare |
7 |
7 |
8 p x = if b1 x |
8 p x = if b1 x |
9 then p (g x) |
9 then p (g x) |
10 else x fi |
10 else x fi |
11 |
11 |