src/CCL/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
child 17456 bcf7544875b2
permissions -rw-r--r--
cleaned up;
wenzelm@9000
     1
(*  Title:      CCL/ROOT.ML
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)";
lcp@997
    10
writeln banner;
lcp@997
    11
lcp@997
    12
print_depth 1;
lcp@997
    13
set eta_contract;
clasohm@0
    14
clasohm@0
    15
(* Higher-Order Set Theory Extension to FOL *)
clasohm@0
    16
(*      used as basis for CCL               *)
clasohm@0
    17
clasohm@121
    18
use_thy "Set";
clasohm@0
    19
use     "subset.ML";
clasohm@0
    20
use     "equalities.ML";
clasohm@0
    21
use     "mono.ML";
clasohm@121
    22
use_thy "Lfp";
clasohm@121
    23
use_thy "Gfp";
clasohm@0
    24
clasohm@0
    25
(* CCL - a computational logic for an untyped functional language *)
clasohm@0
    26
(*                       with evaluation to weak head-normal form *)
clasohm@0
    27
clasohm@121
    28
use_thy "CCL";
clasohm@121
    29
use_thy "Term";
clasohm@121
    30
use_thy "Type";
clasohm@0
    31
use     "coinduction.ML";
clasohm@121
    32
use_thy "Hered";
clasohm@0
    33
clasohm@121
    34
use_thy "Trancl";
clasohm@121
    35
use_thy "Wfd";
clasohm@0
    36
use     "genrec.ML";
clasohm@0
    37
use     "typecheck.ML";
clasohm@0
    38
use     "eval.ML";
clasohm@121
    39
use_thy "Fix";
clasohm@0
    40
lcp@997
    41
print_depth 8;