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 

121

14 
use_thy "Set";

0

15 
use "subset.ML";


16 
use "equalities.ML";


17 
use "mono.ML";

121

18 
use_thy "Lfp";


19 
use_thy "Gfp";

0

20 


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


22 
(* with evaluation to weak headnormal form *)


23 

121

24 
use_thy "CCL";


25 
use_thy "Term";


26 
use_thy "Type";

0

27 
use "coinduction.ML";

121

28 
use_thy "Hered";

0

29 

121

30 
use_thy "Trancl";


31 
use_thy "Wfd";

0

32 
use "genrec.ML";


33 
use "typecheck.ML";


34 
use "eval.ML";

121

35 
use_thy "Fix";

0

36 


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