src/CCL/ROOT.ML
changeset 0 a5a9c433f639
child 59 ab555029f583
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/ROOT.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,37 @@
     1.4 +(*  Title:      CCL/ROOT
     1.5 +    ID:         $Id$
     1.6 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Adds Classical Computational Logic to a database containing First-Order Logic.
    1.10 +*)
    1.11 +
    1.12 +val banner = "Classical Computational Logic (in FOL)";
    1.13 +
    1.14 +(* Higher-Order Set Theory Extension to FOL *)
    1.15 +(*      used as basis for CCL               *)
    1.16 +
    1.17 +use_thy "set";
    1.18 +use     "subset.ML";
    1.19 +use     "equalities.ML";
    1.20 +use     "mono.ML";
    1.21 +use_thy "lfp";
    1.22 +use_thy "gfp";
    1.23 +
    1.24 +(* CCL - a computational logic for an untyped functional language *)
    1.25 +(*                       with evaluation to weak head-normal form *)
    1.26 +
    1.27 +use_thy "ccl";
    1.28 +use_thy "terms";
    1.29 +use_thy "types";
    1.30 +use     "coinduction.ML";
    1.31 +use_thy "hered";
    1.32 +
    1.33 +use_thy "trancl";
    1.34 +use_thy "wf";
    1.35 +use     "genrec.ML";
    1.36 +use     "typecheck.ML";
    1.37 +use     "eval.ML";
    1.38 +use_thy "fix";
    1.39 +
    1.40 +val CCL_build_completed = ();   (*indicate successful build*)