author | wenzelm |
Wed, 13 Jul 2005 16:07:35 +0200 | |
changeset 16813 | 67140ae50e77 |
parent 16483 | ace3c2b95353 |
child 16841 | 228d663cc9b3 |
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; 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";