src/CCL/ROOT.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 59 ab555029f583
permissions -rw-r--r--
Initial revision
     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 First-Order Logic.
     7 *)
     8 
     9 val banner = "Classical Computational Logic (in FOL)";
    10 
    11 (* Higher-Order Set Theory Extension to FOL *)
    12 (*      used as basis for CCL               *)
    13 
    14 use_thy "set";
    15 use     "subset.ML";
    16 use     "equalities.ML";
    17 use     "mono.ML";
    18 use_thy "lfp";
    19 use_thy "gfp";
    20 
    21 (* CCL - a computational logic for an untyped functional language *)
    22 (*                       with evaluation to weak head-normal form *)
    23 
    24 use_thy "ccl";
    25 use_thy "terms";
    26 use_thy "types";
    27 use     "coinduction.ML";
    28 use_thy "hered";
    29 
    30 use_thy "trancl";
    31 use_thy "wf";
    32 use     "genrec.ML";
    33 use     "typecheck.ML";
    34 use     "eval.ML";
    35 use_thy "fix";
    36 
    37 val CCL_build_completed = ();   (*indicate successful build*)