author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14535 | 7cb26928e70d |
child 15188 | 9d57263faf9e |
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"; use_thy "Streams"; print_depth 10;