src/HOL/HOLCF/ROOT.ML
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 40505 src/HOLCF/ROOT.ML@702708d26c9b
child 41413 64cd30d6b0b8
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
wenzelm@3623
     1
(*  Title:      HOLCF/ROOT.ML
clasohm@1461
     2
    Author:     Franz Regensburger
nipkow@243
     3
wenzelm@16841
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     5
*)
nipkow@243
     6
huffman@39982
     7
no_document use_thys ["Nat_Bijection", "Countable"];
nipkow@29921
     8
huffman@40505
     9
use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];