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