changeset 21404 | eb85850d3eb7 |
parent 19763 | ec18656a2c10 |
child 25135 | 4f8176c940cf |
--- a/src/HOLCF/ex/Hoare.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOLCF/ex/Hoare.thy Fri Nov 17 02:20:03 2006 +0100 @@ -30,10 +30,11 @@ g :: "'a -> 'a" definition - p :: "'a -> 'a" + p :: "'a -> 'a" where "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)" - q :: "'a -> 'a" +definition + q :: "'a -> 'a" where "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"