src/CCL/ROOT.ML
author clasohm
Sun Oct 17 16:30:16 1993 +0100 (1993-10-17)
changeset 59 ab555029f583
parent 0 a5a9c433f639
child 72 099d949fe467
permissions -rw-r--r--
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
clasohm@0
     1
(*  Title:      CCL/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Adds Classical Computational Logic to a database containing First-Order Logic.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
val banner = "Classical Computational Logic (in FOL)";
clasohm@0
    10
clasohm@0
    11
(* Higher-Order Set Theory Extension to FOL *)
clasohm@0
    12
(*      used as basis for CCL               *)
clasohm@0
    13
clasohm@59
    14
(*set_load_path [".", "../FOL"]; wait for new Readthy*)
clasohm@59
    15
clasohm@0
    16
use_thy "set";
clasohm@0
    17
use     "subset.ML";
clasohm@0
    18
use     "equalities.ML";
clasohm@0
    19
use     "mono.ML";
clasohm@0
    20
use_thy "lfp";
clasohm@0
    21
use_thy "gfp";
clasohm@0
    22
clasohm@0
    23
(* CCL - a computational logic for an untyped functional language *)
clasohm@0
    24
(*                       with evaluation to weak head-normal form *)
clasohm@0
    25
clasohm@0
    26
use_thy "ccl";
clasohm@59
    27
use_thy "term";
clasohm@59
    28
use_thy "type";
clasohm@0
    29
use     "coinduction.ML";
clasohm@0
    30
use_thy "hered";
clasohm@0
    31
clasohm@0
    32
use_thy "trancl";
clasohm@59
    33
use_thy "wfd";
clasohm@0
    34
use     "genrec.ML";
clasohm@0
    35
use     "typecheck.ML";
clasohm@0
    36
use     "eval.ML";
clasohm@0
    37
use_thy "fix";
clasohm@0
    38
clasohm@0
    39
val CCL_build_completed = ();   (*indicate successful build*)