use all files in HOLCF.thy;
authorwenzelm
Thu Jul 14 19:28:23 2005 +0200 (2005-07-14)
changeset 16841228d663cc9b3
parent 16840 3d5aad11bc24
child 16842 5979c46853d1
use all files in HOLCF.thy;
src/HOLCF/HOLCF.ML
src/HOLCF/HOLCF.thy
src/HOLCF/ROOT.ML
     1.1 --- a/src/HOLCF/HOLCF.ML	Thu Jul 14 19:28:22 2005 +0200
     1.2 +++ b/src/HOLCF/HOLCF.ML	Thu Jul 14 19:28:23 2005 +0200
     1.3 @@ -1,16 +1,8 @@
     1.4  (*  Title:      HOLCF/HOLCF.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7  *)
     1.8  
     1.9  structure HOLCF =
    1.10  struct
    1.11    val thy = the_context ();
    1.12  end;
    1.13 -
    1.14 -use "adm_tac.ML";
    1.15 -
    1.16 -simpset_ref() := simpset() addSolver
    1.17 -   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
    1.18 -
    1.19 -val HOLCF_ss = simpset();
     2.1 --- a/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:22 2005 +0200
     2.2 +++ b/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:23 2005 +0200
     2.3 @@ -2,11 +2,27 @@
     2.4      ID:         $Id$
     2.5      Author:     Franz Regensburger
     2.6  
     2.7 -Top theory for HOLCF system.
     2.8 +HOLCF -- a semantic extension of HOL by the LCF logic.
     2.9  *)
    2.10  
    2.11  theory HOLCF
    2.12  imports Sprod Ssum Up Lift Discrete One Tr Domain
    2.13 +uses
    2.14 +  "holcf_logic.ML"
    2.15 +  "cont_consts.ML"
    2.16 +  "domain/library.ML"
    2.17 +  "domain/syntax.ML"
    2.18 +  "domain/axioms.ML"
    2.19 +  "domain/theorems.ML"
    2.20 +  "domain/extender.ML"
    2.21 +  "domain/interface.ML"
    2.22 +  "adm_tac.ML"
    2.23 +
    2.24  begin
    2.25  
    2.26 +ML_setup {*
    2.27 +  simpset_ref() := simpset() addSolver
    2.28 +     (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
    2.29 +*}
    2.30 +
    2.31  end
     3.1 --- a/src/HOLCF/ROOT.ML	Thu Jul 14 19:28:22 2005 +0200
     3.2 +++ b/src/HOLCF/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
     3.3 @@ -2,23 +2,10 @@
     3.4      ID:         $Id$
     3.5      Author:     Franz Regensburger
     3.6  
     3.7 -Conservative (semantic) extension of HOL by the LCF logic.
     3.8 +HOLCF -- a semantic extension of HOL by the LCF logic.
     3.9  *)
    3.10  
    3.11  val banner = "HOLCF";
    3.12  writeln banner;
    3.13  
    3.14  use_thy "HOLCF";
    3.15 -
    3.16 -use "holcf_logic.ML";
    3.17 -use "cont_consts.ML";
    3.18 -
    3.19 -(* domain package *)
    3.20 -use "domain/library.ML";
    3.21 -use "domain/syntax.ML";
    3.22 -use "domain/axioms.ML";
    3.23 -use "domain/theorems.ML";
    3.24 -use "domain/extender.ML";
    3.25 -use "domain/interface.ML";
    3.26 -
    3.27 -path_add "~~/src/HOLCF/ex";