equal
deleted
inserted
replaced
1 (* Title: CCL/ROOT.ML |
1 (* Title: CCL/ROOT.ML |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 |
4 |
5 Classical Computational Logic based on First-Order Logic. |
5 Classical Computational Logic based on First-Order Logic. |
|
6 |
|
7 A computational logic for an untyped functional language with |
|
8 evaluation to weak head-normal form. |
6 *) |
9 *) |
7 |
10 |
8 set eta_contract; |
11 Unsynchronized.set eta_contract; |
9 |
|
10 (* CCL - a computational logic for an untyped functional language *) |
|
11 (* with evaluation to weak head-normal form *) |
|
12 |
12 |
13 use_thys ["Wfd", "Fix"]; |
13 use_thys ["Wfd", "Fix"]; |
14 |
|