| changeset 1150 | 66512c9e6bd6 |
| parent 442 | 13ac1fd0a14d |
| child 1168 | 74be52691d62 |
| 1149:5750eba8820d | 1150:66512c9e6bd6 |
|---|---|
17 |
17 |
18 rules |
18 rules |
19 |
19 |
20 inst_cfun_pcpo "(UU::'a->'b) = UU_cfun" |
20 inst_cfun_pcpo "(UU::'a->'b) = UU_cfun" |
21 |
21 |
22 Istrictify_def "Istrictify(f,x) == (@z.\ |
22 Istrictify_def "Istrictify(f,x) == (@z. |
23 \ ( x=UU --> z = UU)\ |
23 ( x=UU --> z = UU) |
24 \ & (~x=UU --> z = f[x]))" |
24 & (~x=UU --> z = f[x]))" |
25 |
25 |
26 strictify_def "strictify == (LAM f x.Istrictify(f,x))" |
26 strictify_def "strictify == (LAM f x.Istrictify(f,x))" |
27 |
27 |
28 end |
28 end |
29 |
29 |