equal
deleted
inserted
replaced
1 (* Title: HOLCF/ex/hoare.thy |
1 (* Title: HOL/HOLCF/ex/Hoare.thy |
2 Author: Franz Regensburger |
2 Author: Franz Regensburger |
3 |
3 |
4 Theory for an example by C.A.R. Hoare |
4 Theory for an example by C.A.R. Hoare |
5 |
5 |
6 p x = if b1 x |
6 p x = if b1 x |