| changeset 2379 | 2e55b396e24c |
| parent 1479 | 21eb5e156d91 |
| child 2380 | 90280b3a538b |
| 2378:fc103154ad8f | 2379:2e55b396e24c |
|---|---|
19 In order to get a nice notation we fix the functions b1,b2 and g in the |
19 In order to get a nice notation we fix the functions b1,b2 and g in the |
20 signature of this example |
20 signature of this example |
21 |
21 |
22 *) |
22 *) |
23 |
23 |
24 Hoare = Tr2 + |
24 Hoare = HOLCF + |
25 |
25 |
26 consts |
26 consts |
27 b1:: "'a -> tr" |
27 b1:: "'a -> tr" |
28 b2:: "'a -> tr" |
28 b2:: "'a -> tr" |
29 g:: "'a -> 'a" |
29 g:: "'a -> 'a" |