author clasohm
Tue, 21 Nov 1995 15:10:12 +0100
changeset 1361 90d615b599d9
parent 1293 4ade5d1d369c
child 6349 f7750d816c21
permissions -rw-r--r--
main directory is now read by exit_use_dir, too; removed make_chart from ROOT.ML

(*  Title:      CCL/ROOT
    ID:         $Id$
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Adds Classical Computational Logic to a database containing First-Order Logic.

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

print_depth 1;
set eta_contract;

(* Higher-Order Set Theory Extension to FOL *)
(*      used as basis for CCL               *)

use_thy "Set";
use     "subset.ML";
use     "equalities.ML";
use     "mono.ML";
use_thy "Lfp";
use_thy "Gfp";

(* CCL - a computational logic for an untyped functional language *)
(*                       with evaluation to weak head-normal form *)

use_thy "CCL";
use_thy "Term";
use_thy "Type";
use     "coinduction.ML";
use_thy "Hered";

use_thy "Trancl";
use_thy "Wfd";
use     "genrec.ML";
use     "typecheck.ML";
use     "eval.ML";
use_thy "Fix";

print_depth 8;

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