| changeset 39128 | 93a7365fb4ee |
| parent 38798 | 89f273ab1d42 |
| 39127:e7ecbe86d22e | 39128:93a7365fb4ee |
|---|---|
6 |
6 |
7 A computational logic for an untyped functional language with |
7 A computational logic for an untyped functional language with |
8 evaluation to weak head-normal form. |
8 evaluation to weak head-normal form. |
9 *) |
9 *) |
10 |
10 |
11 eta_contract := true; |
|
12 |
|
13 use_thys ["Wfd", "Fix"]; |
11 use_thys ["Wfd", "Fix"]; |