src/CCL/ROOT.ML
author clasohm
Tue Nov 21 15:10:12 1995 +0100 (1995-11-21)
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
     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 writeln banner;
    11 
    12 print_depth 1;
    13 set eta_contract;
    14 
    15 (* Higher-Order Set Theory Extension to FOL *)
    16 (*      used as basis for CCL               *)
    17 
    18 use_thy "Set";
    19 use     "subset.ML";
    20 use     "equalities.ML";
    21 use     "mono.ML";
    22 use_thy "Lfp";
    23 use_thy "Gfp";
    24 
    25 (* CCL - a computational logic for an untyped functional language *)
    26 (*                       with evaluation to weak head-normal form *)
    27 
    28 use_thy "CCL";
    29 use_thy "Term";
    30 use_thy "Type";
    31 use     "coinduction.ML";
    32 use_thy "Hered";
    33 
    34 use_thy "Trancl";
    35 use_thy "Wfd";
    36 use     "genrec.ML";
    37 use     "typecheck.ML";
    38 use     "eval.ML";
    39 use_thy "Fix";
    40 
    41 print_depth 8;
    42 
    43 val CCL_build_completed = ();   (*indicate successful build*)