src/HOLCF/ROOT.ML
author clasohm
Wed Oct 04 14:01:44 1995 +0100 (1995-10-04)
changeset 1267 bca91b4e1710
parent 1168 74be52691d62
child 1274 ea0668a1c0ba
permissions -rw-r--r--
added local simpsets
     1 (*  Title:	HOLCF/ROOT
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright	1993 Technische Universitaet Muenchen
     5 
     6 ROOT file for the conservative extension of HOL by the LCF logic.
     7 Should be executed in subdirectory HOLCF.
     8 *)
     9 
    10 val banner = "Higher-order Logic of Computable Functions; curried version";
    11 writeln banner;
    12 print_depth 1;
    13 
    14 init_thy_reader();
    15 
    16 use_thy "Fix";
    17 use_thy "Dlist";
    18 
    19 use "../Pure/install_pp.ML";
    20 print_depth 8;  
    21 
    22 val HOLCF_build_completed = ();	(*indicate successful build*)