changeset 38798 | 89f273ab1d42 |
parent 32740 | 9dd0a2f83429 |
child 39128 | 93a7365fb4ee |
38797:abe92b33ac9f | 38798:89f273ab1d42 |
---|---|
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 Unsynchronized.set eta_contract; |
11 eta_contract := true; |
12 |
12 |
13 use_thys ["Wfd", "Fix"]; |
13 use_thys ["Wfd", "Fix"]; |