| changeset 1168 | 74be52691d62 |
| parent 1150 | 66512c9e6bd6 |
| child 1479 | 21eb5e156d91 |
| 1167:cbd32a0f2f41 | 1168:74be52691d62 |
|---|---|
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 defs |
23 ( x=UU --> z = UU) |
|
24 & (~x=UU --> z = f[x]))" |
|
25 |
23 |
26 strictify_def "strictify == (LAM f x.Istrictify(f,x))" |
24 Istrictify_def "Istrictify f x == if x=UU then UU else f`x" |
25 |
|
26 strictify_def "strictify == (LAM f x.Istrictify f x)" |
|
27 |
27 |
28 end |
28 end |
29 |
29 |
30 |
|
31 |