# HG changeset patch # User wenzelm # Date 1121362103 -7200 # Node ID 228d663cc9b350e05063542c433e833c2ef3eb15 # Parent 3d5aad11bc247f38e2541fe8095444ca8aa3c3f9 use all files in HOLCF.thy; diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/HOLCF.ML --- a/src/HOLCF/HOLCF.ML Thu Jul 14 19:28:22 2005 +0200 +++ b/src/HOLCF/HOLCF.ML Thu Jul 14 19:28:23 2005 +0200 @@ -1,16 +1,8 @@ (* Title: HOLCF/HOLCF.ML ID: $Id$ - Author: Franz Regensburger *) structure HOLCF = struct val thy = the_context (); end; - -use "adm_tac.ML"; - -simpset_ref() := simpset() addSolver - (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); - -val HOLCF_ss = simpset(); diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Thu Jul 14 19:28:22 2005 +0200 +++ b/src/HOLCF/HOLCF.thy Thu Jul 14 19:28:23 2005 +0200 @@ -2,11 +2,27 @@ ID: $Id$ Author: Franz Regensburger -Top theory for HOLCF system. +HOLCF -- a semantic extension of HOL by the LCF logic. *) theory HOLCF imports Sprod Ssum Up Lift Discrete One Tr Domain +uses + "holcf_logic.ML" + "cont_consts.ML" + "domain/library.ML" + "domain/syntax.ML" + "domain/axioms.ML" + "domain/theorems.ML" + "domain/extender.ML" + "domain/interface.ML" + "adm_tac.ML" + begin +ML_setup {* + simpset_ref() := simpset() addSolver + (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); +*} + end diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/ROOT.ML --- a/src/HOLCF/ROOT.ML Thu Jul 14 19:28:22 2005 +0200 +++ b/src/HOLCF/ROOT.ML Thu Jul 14 19:28:23 2005 +0200 @@ -2,23 +2,10 @@ ID: $Id$ Author: Franz Regensburger -Conservative (semantic) extension of HOL by the LCF logic. +HOLCF -- a 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";