1.1 --- a/src/HOLCF/Domain.thy	Wed Apr 08 20:29:15 2009 +0200
     1.2 +++ b/src/HOLCF/Domain.thy	Fri Apr 10 11:35:21 2009 -0700
     1.3 @@ -6,6 +6,14 @@
     1.4  
     1.5  theory Domain
     1.6  imports Ssum Sprod Up One Tr Fixrec
     1.7 +uses
     1.8 +  ("Tools/cont_consts.ML")
     1.9 +  ("Tools/cont_proc.ML")
    1.10 +  ("Tools/domain/domain_library.ML")
    1.11 +  ("Tools/domain/domain_syntax.ML")
    1.12 +  ("Tools/domain/domain_axioms.ML")
    1.13 +  ("Tools/domain/domain_theorems.ML")
    1.14 +  ("Tools/domain/domain_extender.ML")
    1.15  begin
    1.16  
    1.17  defaultsort pcpo
    1.18 @@ -193,4 +201,15 @@
    1.19  
    1.20  lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
    1.21  
    1.22 +
    1.23 +subsection {* Installing the domain package *}
    1.24 +
    1.25 +use "Tools/cont_consts.ML"
    1.26 +use "Tools/cont_proc.ML"
    1.27 +use "Tools/domain/domain_library.ML"
    1.28 +use "Tools/domain/domain_syntax.ML"
    1.29 +use "Tools/domain/domain_axioms.ML"
    1.30 +use "Tools/domain/domain_theorems.ML"
    1.31 +use "Tools/domain/domain_extender.ML"
    1.32 +
    1.33  end

     2.1 --- a/src/HOLCF/HOLCF.thy	Wed Apr 08 20:29:15 2009 +0200
     2.2 +++ b/src/HOLCF/HOLCF.thy	Fri Apr 10 11:35:21 2009 -0700
     2.3 @@ -9,13 +9,6 @@
     2.4    Domain ConvexPD Algebraic Universal Sum_Cpo Main
     2.5  uses
     2.6    "holcf_logic.ML"
     2.7 -  "Tools/cont_consts.ML"
     2.8 -  "Tools/cont_proc.ML"
     2.9 -  "Tools/domain/domain_library.ML"
    2.10 -  "Tools/domain/domain_syntax.ML"
    2.11 -  "Tools/domain/domain_axioms.ML"
    2.12 -  "Tools/domain/domain_theorems.ML"
    2.13 -  "Tools/domain/domain_extender.ML"
    2.14    "Tools/adm_tac.ML"
    2.15  begin
    2.16  

     3.1 --- a/src/HOLCF/Tools/cont_consts.ML	Wed Apr 08 20:29:15 2009 +0200
     3.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Fri Apr 10 11:35:21 2009 -0700
     3.3 @@ -18,8 +18,6 @@
     3.4  
     3.5  (* misc utils *)
     3.6  
     3.7 -open HOLCFLogic;
     3.8 -
     3.9  fun first  (x,_,_) = x;
    3.10  fun second (_,x,_) = x;
    3.11  fun third  (_,_,x) = x;
    3.12 @@ -66,7 +64,7 @@
    3.13              (c2,change_arrow n T,mx   ),
    3.14              trans_rules c2 c n mx) end;
    3.15  
    3.16 -fun cfun_arity (Type(n,[_,T])) = if n = cfun_arrow then 1+cfun_arity T else 0
    3.17 +fun cfun_arity (Type(n,[_,T])) = if n = @{type_name "->"} then 1+cfun_arity T else 0
    3.18  |   cfun_arity _               = 0;
    3.19  
    3.20  fun is_contconst (_,_,NoSyn   ) = false

     4.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Apr 08 20:29:15 2009 +0200
     4.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri Apr 10 11:35:21 2009 -0700
     4.3 @@ -34,8 +34,6 @@
     4.4  
     4.5  structure Domain_Library = struct
     4.6  
     4.7 -open HOLCFLogic;
     4.8 -
     4.9  exception Impossible of string;
    4.10  fun Imposs msg = raise Impossible ("Domain:"^msg);
    4.11  
    4.12 @@ -72,7 +70,7 @@
    4.13        | index_vnames([],occupied) = [];
    4.14  in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
    4.15  
    4.16 -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
    4.17 +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
    4.18  fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
    4.19  
    4.20  (* ----- constructor list handling ----- *)
    4.21 @@ -99,6 +97,17 @@
    4.22  (* ----- support for type and mixfix expressions ----- *)
    4.23  
    4.24  infixr 5 -->;
    4.25 +fun mk_uT T = Type(@{type_name "u"}, [T]);
    4.26 +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    4.27 +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
    4.28 +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
    4.29 +val oneT = @{typ one};
    4.30 +val trT = @{typ tr};
    4.31 +
    4.32 +infixr 6 ->>;
    4.33 +val op ->> = mk_cfunT;
    4.34 +
    4.35 +fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
    4.36  
    4.37  (* ----- support for term expressions ----- *)
    4.38