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

(*  Title:      CCL/ROOT
    ID:         $Id$
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Adds Classical Computational Logic to a database containing First-Order Logic.

val banner = "Classical Computational Logic (in FOL)";

(* Higher-Order Set Theory Extension to FOL *)
(*      used as basis for CCL               *)

set_loadpath [".", "../FOL"];

use_thy "set";
use     "subset.ML";
use     "equalities.ML";
use     "mono.ML";
use_thy "lfp";
use_thy "gfp";

(* CCL - a computational logic for an untyped functional language *)
(*                       with evaluation to weak head-normal form *)

use_thy "ccl";
use_thy "term";
use_thy "type";
use     "coinduction.ML";
use_thy "hered";

use_thy "trancl";
use_thy "wfd";
use     "genrec.ML";
use     "typecheck.ML";
use     "eval.ML";
use_thy "fix";

val CCL_build_completed = ();   (*indicate successful build*)