src/HOLCF/ROOT.ML
author huffman
Mon, 08 Nov 2010 15:13:45 -0800
changeset 40487 1320a0747974
parent 39982 5681f840688b
child 40505 702708d26c9b
permissions -rw-r--r--
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data

(*  Title:      HOLCF/ROOT.ML
    Author:     Franz Regensburger

HOLCF -- a semantic extension of HOL by the LCF logic.
*)

no_document use_thys ["Nat_Bijection", "Countable"];

use_thys ["HOLCF"];