author  clasohm 
Sun, 17 Oct 1993 16:30:16 +0100  
changeset 59  ab555029f583 
parent 0  a5a9c433f639 
child 72  099d949fe467 
permissions  rwrr 
0  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 FirstOrder Logic. 

7 
*) 

8 

9 
val banner = "Classical Computational Logic (in FOL)"; 

10 

11 
(* HigherOrder Set Theory Extension to FOL *) 

12 
(* used as basis for CCL *) 

13 

59
ab555029f583
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm
parents:
0
diff
changeset

14 
(*set_load_path [".", "../FOL"]; wait for new Readthy*) 
ab555029f583
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm
parents:
0
diff
changeset

15 

0  16 
use_thy "set"; 
17 
use "subset.ML"; 

18 
use "equalities.ML"; 

19 
use "mono.ML"; 

20 
use_thy "lfp"; 

21 
use_thy "gfp"; 

22 

23 
(* CCL  a computational logic for an untyped functional language *) 

24 
(* with evaluation to weak headnormal form *) 

25 

26 
use_thy "ccl"; 

59
ab555029f583
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm
parents:
0
diff
changeset

27 
use_thy "term"; 
ab555029f583
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm
parents:
0
diff
changeset

28 
use_thy "type"; 
0  29 
use "coinduction.ML"; 
30 
use_thy "hered"; 

31 

32 
use_thy "trancl"; 

59
ab555029f583
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm
parents:
0
diff
changeset

33 
use_thy "wfd"; 
0  34 
use "genrec.ML"; 
35 
use "typecheck.ML"; 

36 
use "eval.ML"; 

37 
use_thy "fix"; 

38 

39 
val CCL_build_completed = (); (*indicate successful build*) 