author | wenzelm |
Tue, 18 Jul 2006 02:22:38 +0200 | |
changeset 20140 | 98acc6d0fab6 |
parent 17456 | bcf7544875b2 |
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"; |