src/CCL/ROOT.ML
author wenzelm
Sat Sep 17 17:35:26 2005 +0200 (2005-09-17)
changeset 17456 bcf7544875b2
parent 9000 c20d58286a51
child 20140 98acc6d0fab6
permissions -rw-r--r--
converted to Isar theory format;
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
wenzelm@17456
     6
Classical Computational Logic based on 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
set eta_contract;
clasohm@0
    13
clasohm@0
    14
(* CCL - a computational logic for an untyped functional language *)
clasohm@0
    15
(*                       with evaluation to weak head-normal form *)
clasohm@0
    16
clasohm@121
    17
use_thy "CCL";
clasohm@121
    18
use_thy "Hered";
clasohm@121
    19
use_thy "Wfd";
clasohm@121
    20
use_thy "Fix";