equal
deleted
inserted
replaced
|
1 (* Title: CCL/ROOT |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Adds Classical Computational Logic to a database containing First-Order Logic. |
|
7 *) |
|
8 |
|
9 val banner = "Classical Computational Logic (in FOL)"; |
|
10 |
|
11 (* Higher-Order Set Theory Extension to FOL *) |
|
12 (* used as basis for CCL *) |
|
13 |
|
14 use_thy "set"; |
|
15 use "subset.ML"; |
|
16 use "equalities.ML"; |
|
17 use "mono.ML"; |
|
18 use_thy "lfp"; |
|
19 use_thy "gfp"; |
|
20 |
|
21 (* CCL - a computational logic for an untyped functional language *) |
|
22 (* with evaluation to weak head-normal form *) |
|
23 |
|
24 use_thy "ccl"; |
|
25 use_thy "terms"; |
|
26 use_thy "types"; |
|
27 use "coinduction.ML"; |
|
28 use_thy "hered"; |
|
29 |
|
30 use_thy "trancl"; |
|
31 use_thy "wf"; |
|
32 use "genrec.ML"; |
|
33 use "typecheck.ML"; |
|
34 use "eval.ML"; |
|
35 use_thy "fix"; |
|
36 |
|
37 val CCL_build_completed = (); (*indicate successful build*) |