src/HOLCF/ROOT.ML
author oheimb
Mon Apr 12 12:18:48 2004 +0200 (2004-04-12)
changeset 14535 7cb26928e70d
parent 12036 49f6c49454c2
child 14981 e73f8140af78
permissions -rw-r--r--
added Streams.thy (with stream concatenation etc.)
wenzelm@3623
     1
(*  Title:      HOLCF/ROOT.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
wenzelm@12036
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243
     5
wenzelm@12036
     6
Conservative (semantic) extension of HOL by the LCF logic.
nipkow@243
     7
*)
nipkow@243
     8
wenzelm@3623
     9
val banner = "HOLCF";
oheimb@2394
    10
writeln banner;
regensbu@1274
    11
nipkow@243
    12
print_depth 1;
nipkow@243
    13
regensbu@1274
    14
use_thy "HOLCF";
regensbu@1274
    15
wenzelm@4129
    16
use "holcf_logic.ML";
wenzelm@4129
    17
use "cont_consts.ML";
regensbu@1274
    18
oheimb@4122
    19
(* domain package *)
regensbu@1285
    20
use "domain/library.ML";
regensbu@1285
    21
use "domain/syntax.ML";
regensbu@1285
    22
use "domain/axioms.ML";
regensbu@1285
    23
use "domain/theorems.ML";
regensbu@1285
    24
use "domain/extender.ML";
regensbu@1285
    25
use "domain/interface.ML";
nipkow@297
    26
oheimb@14535
    27
path_add "~~/src/HOLCF/ex";
oheimb@14535
    28
use_thy "Streams";
oheimb@14535
    29
oheimb@2394
    30
print_depth 10;