author | aspinall |
Mon, 04 Dec 2006 20:40:11 +0100 | |
changeset 21637 | a7b156c404e2 |
parent 20140 | 98acc6d0fab6 |
child 24106 | f2965bf954dc |
permissions | -rw-r--r-- |
9000 | 1 |
(* Title: CCL/ROOT.ML |
0 | 2 |
ID: $Id$ |
3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
17456 | 6 |
Classical Computational Logic based on First-Order Logic. |
0 | 7 |
*) |
8 |
||
9 |
val banner = "Classical Computational Logic (in FOL)"; |
|
997 | 10 |
writeln banner; |
11 |
||
12 |
set eta_contract; |
|
0 | 13 |
|
14 |
(* CCL - a computational logic for an untyped functional language *) |
|
15 |
(* with evaluation to weak head-normal form *) |
|
16 |
||
121 | 17 |
use_thy "Wfd"; |
18 |
use_thy "Fix"; |