author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 15188 | 9d57263faf9e |
child 16483 | ace3c2b95353 |
permissions | -rw-r--r-- |
(* Title: HOLCF/ROOT.ML ID: $Id$ Author: Franz Regensburger Conservative (semantic) extension of HOL by the LCF logic. *) val banner = "HOLCF"; writeln banner; print_depth 1; use_thy "HOLCF"; use "holcf_logic.ML"; use "cont_consts.ML"; (* domain package *) use "domain/library.ML"; use "domain/syntax.ML"; use "domain/axioms.ML"; use "domain/theorems.ML"; use "domain/extender.ML"; use "domain/interface.ML"; path_add "~~/src/HOLCF/ex"; print_depth 10;