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 


6 
Adds Classical Computational Logic to a database containing FirstOrder Logic.


7 
*)


8 


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

997

10 
writeln banner;


11 


12 
print_depth 1;


13 
set eta_contract;

0

14 


15 
(* HigherOrder Set Theory Extension to FOL *)


16 
(* used as basis for CCL *)


17 

121

18 
use_thy "Set";

0

19 
use "subset.ML";


20 
use "equalities.ML";


21 
use "mono.ML";

121

22 
use_thy "Lfp";


23 
use_thy "Gfp";

0

24 


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


26 
(* with evaluation to weak headnormal form *)


27 

121

28 
use_thy "CCL";


29 
use_thy "Term";


30 
use_thy "Type";

0

31 
use "coinduction.ML";

121

32 
use_thy "Hered";

0

33 

121

34 
use_thy "Trancl";


35 
use_thy "Wfd";

0

36 
use "genrec.ML";


37 
use "typecheck.ML";


38 
use "eval.ML";

121

39 
use_thy "Fix";

0

40 

997

41 
print_depth 8;
