src/HOLCF/ROOT.ML
author wenzelm
Thu May 19 17:06:24 1994 +0200 (1994-05-19)
changeset 393 02b27671b899
parent 297 5ef75ff3baeb
child 625 119391dd1d59
permissions -rw-r--r--
thy reader now initialised by init_thy_reader();
nipkow@243
     1
(*  Title:	HOLCF/ROOT
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright	1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
ROOT file for the conservative extension of HOL by the LCF logic.
nipkow@243
     7
Should be executed in subdirectory HOLCF.
nipkow@243
     8
*)
nipkow@243
     9
nipkow@243
    10
val banner = "Higher-order Logic of Computable Functions";
nipkow@243
    11
writeln banner;
nipkow@243
    12
print_depth 1;
nipkow@243
    13
wenzelm@393
    14
init_thy_reader();
nipkow@243
    15
nipkow@243
    16
use_thy "Holcfb";
nipkow@243
    17
use_thy "Void";
nipkow@297
    18
nipkow@297
    19
use_thy "Porder0";
nipkow@243
    20
use_thy "Porder";
nipkow@297
    21
nipkow@243
    22
use_thy "Pcpo";
nipkow@243
    23
nipkow@243
    24
use_thy "Fun1";
nipkow@243
    25
use_thy "Fun2";
nipkow@243
    26
use_thy "Fun3";
nipkow@243
    27
nipkow@243
    28
use_thy "Cont";
nipkow@243
    29
nipkow@243
    30
use_thy "Cfun1";
nipkow@243
    31
use_thy "Cfun2";
nipkow@243
    32
use_thy "Cfun3";
nipkow@243
    33
nipkow@243
    34
use_thy "Cprod1";
nipkow@243
    35
use_thy "Cprod2";
nipkow@243
    36
use_thy "Cprod3";
nipkow@243
    37
nipkow@243
    38
use_thy "Sprod0";
nipkow@243
    39
use_thy "Sprod1"; 
nipkow@243
    40
use_thy "Sprod2"; 
nipkow@243
    41
use_thy "Sprod3"; 
nipkow@243
    42
nipkow@243
    43
use_thy "Ssum0";
nipkow@243
    44
use_thy "Ssum1";
nipkow@243
    45
use_thy "Ssum2";
nipkow@243
    46
use_thy "Ssum3";
nipkow@243
    47
nipkow@243
    48
use_thy "Lift1";
nipkow@243
    49
use_thy "Lift2";
nipkow@243
    50
use_thy "Lift3";
nipkow@243
    51
nipkow@243
    52
use_thy "Fix";
nipkow@243
    53
nipkow@243
    54
use_thy "ccc1";
nipkow@243
    55
use_thy "One";
nipkow@243
    56
use_thy "Tr1";
nipkow@243
    57
use_thy "Tr2";
nipkow@243
    58
nipkow@243
    59
use_thy "HOLCF";
nipkow@243
    60
nipkow@243
    61
use_thy "Dnat";
nipkow@243
    62
use_thy "Dnat2";
nipkow@243
    63
use_thy "Stream";
nipkow@243
    64
use_thy "Stream2";
nipkow@297
    65
use_thy "Dlist";
nipkow@297
    66
nipkow@243
    67
nipkow@243
    68
use "../Pure/install_pp.ML";
nipkow@243
    69
print_depth 8;  
nipkow@243
    70
nipkow@243
    71
val HOLCF_build_completed = ();	(*indicate successful build*)