discontinued ancient tradition to suffix certain ML module names with "_package"
authorhaftmann
Sun Jun 21 08:38:58 2009 +0200 (2009-06-21)
changeset 317387b9b9ba532ca
parent 31737 b3f63611784e
child 31739 8155c4d94354
child 31742 5fb12f859de6
discontinued ancient tradition to suffix certain ML module names with "_package"
src/HOLCF/Fixrec.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/IsaMakefile
src/HOLCF/Pcpodef.thy
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef_package.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Sun Jun 21 08:38:58 2009 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sun Jun 21 08:38:58 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Fixrec
     1.6  imports Sprod Ssum Up One Tr Fix
     1.7 -uses ("Tools/fixrec_package.ML")
     1.8 +uses ("Tools/fixrec.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Maybe monad type *}
    1.12 @@ -599,12 +599,12 @@
    1.13  
    1.14  subsection {* Initializing the fixrec package *}
    1.15  
    1.16 -use "Tools/fixrec_package.ML"
    1.17 +use "Tools/fixrec.ML"
    1.18  
    1.19 -setup {* FixrecPackage.setup *}
    1.20 +setup {* Fixrec.setup *}
    1.21  
    1.22  setup {*
    1.23 -  FixrecPackage.add_matchers
    1.24 +  Fixrec.add_matchers
    1.25      [ (@{const_name up}, @{const_name match_up}),
    1.26        (@{const_name sinl}, @{const_name match_sinl}),
    1.27        (@{const_name sinr}, @{const_name match_sinr}),
     2.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 08:38:58 2009 +0200
     2.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sun Jun 21 08:38:58 2009 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  theory Abstraction
     2.6  imports LiveIOA
     2.7 -uses ("ioa_package.ML")
     2.8 +uses ("ioa.ML")
     2.9  begin
    2.10  
    2.11  defaultsort type
    2.12 @@ -613,6 +613,6 @@
    2.13  
    2.14  method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
    2.15  
    2.16 -use "ioa_package.ML"
    2.17 +use "ioa.ML"
    2.18  
    2.19  end
     3.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 08:38:58 2009 +0200
     3.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 08:38:58 2009 +0200
     3.3 @@ -1,9 +1,8 @@
     3.4 -(*  Title:      HOLCF/IOA/meta_theory/ioa_package.ML
     3.5 -    ID:         $Id$
     3.6 +(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
     3.7      Author:     Tobias Hamberger, TU Muenchen
     3.8  *)
     3.9  
    3.10 -signature IOA_PACKAGE =
    3.11 +signature IOA =
    3.12  sig
    3.13    val add_ioa: string -> string
    3.14      -> (string) list -> (string) list -> (string) list
    3.15 @@ -16,7 +15,7 @@
    3.16    val add_rename : string -> string -> string -> theory -> theory
    3.17  end;
    3.18  
    3.19 -structure IoaPackage: IOA_PACKAGE =
    3.20 +structure Ioa: IOA =
    3.21  struct
    3.22  
    3.23  val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
     4.1 --- a/src/HOLCF/IsaMakefile	Sun Jun 21 08:38:58 2009 +0200
     4.2 +++ b/src/HOLCF/IsaMakefile	Sun Jun 21 08:38:58 2009 +0200
     4.3 @@ -67,8 +67,8 @@
     4.4    Tools/domain/domain_library.ML \
     4.5    Tools/domain/domain_syntax.ML \
     4.6    Tools/domain/domain_theorems.ML \
     4.7 -  Tools/fixrec_package.ML \
     4.8 -  Tools/pcpodef_package.ML \
     4.9 +  Tools/fixrec.ML \
    4.10 +  Tools/pcpodef.ML \
    4.11    holcf_logic.ML \
    4.12    document/root.tex
    4.13  	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
    4.14 @@ -127,7 +127,7 @@
    4.15    IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \
    4.16    IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
    4.17    IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
    4.18 -  IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
    4.19 +  IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
    4.20  	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
    4.21  
    4.22  
     5.1 --- a/src/HOLCF/Pcpodef.thy	Sun Jun 21 08:38:58 2009 +0200
     5.2 +++ b/src/HOLCF/Pcpodef.thy	Sun Jun 21 08:38:58 2009 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  theory Pcpodef
     5.6  imports Adm
     5.7 -uses ("Tools/pcpodef_package.ML")
     5.8 +uses ("Tools/pcpodef.ML")
     5.9  begin
    5.10  
    5.11  subsection {* Proving a subtype is a partial order *}
    5.12 @@ -303,6 +303,6 @@
    5.13  
    5.14  subsection {* HOLCF type definition package *}
    5.15  
    5.16 -use "Tools/pcpodef_package.ML"
    5.17 +use "Tools/pcpodef.ML"
    5.18  
    5.19  end
     6.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 08:38:58 2009 +0200
     6.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Jun 21 08:38:58 2009 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  
     6.5  signature DOMAIN_AXIOMS =
     6.6  sig
     6.7 -  val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
     6.8 +  val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
     6.9  
    6.10    val calc_axioms :
    6.11        string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
    6.12 @@ -171,7 +171,7 @@
    6.13        val mat_names = map mat_name con_names;
    6.14        fun qualify n = Sign.full_name thy (Binding.name n);
    6.15        val ms = map qualify con_names ~~ map qualify mat_names;
    6.16 -    in FixrecPackage.add_matchers ms thy end;
    6.17 +    in Fixrec.add_matchers ms thy end;
    6.18  
    6.19  fun add_axioms comp_dnam (eqs : eq list) thy' =
    6.20      let
     7.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 08:38:58 2009 +0200
     7.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun Jun 21 08:38:58 2009 +0200
     7.3 @@ -135,10 +135,10 @@
     7.4        eqtype arg;
     7.5    type cons = string * arg list;
     7.6    type eq = (string * typ list) * cons list;
     7.7 -  val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
     7.8 +  val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
     7.9    val is_lazy : arg -> bool;
    7.10    val rec_of : arg -> int;
    7.11 -  val dtyp_of : arg -> DatatypeAux.dtyp;
    7.12 +  val dtyp_of : arg -> Datatype.dtyp;
    7.13    val sel_of : arg -> string option;
    7.14    val vname : arg -> string;
    7.15    val upd_vname : (string -> string) -> arg -> arg;
    7.16 @@ -154,7 +154,7 @@
    7.17    val idx_name : 'a list -> string -> int -> string;
    7.18    val app_rec_arg : (int -> term) -> arg -> term;
    7.19    val con_app : string -> arg list -> term;
    7.20 -  val dtyp_of_eq : eq -> DatatypeAux.dtyp;
    7.21 +  val dtyp_of_eq : eq -> Datatype.dtyp;
    7.22  
    7.23  
    7.24    (* Name mangling *)
    7.25 @@ -215,7 +215,7 @@
    7.26  (* ----- constructor list handling ----- *)
    7.27  
    7.28  type arg =
    7.29 -     (bool * DatatypeAux.dtyp) *   (*  (lazy, recursive element) *)
    7.30 +     (bool * Datatype.dtyp) *   (*  (lazy, recursive element) *)
    7.31       string option *               (*   selector name    *)
    7.32       string;                       (*   argument name    *)
    7.33  
     8.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 08:38:58 2009 +0200
     8.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 08:38:58 2009 +0200
     8.3 @@ -1,10 +1,10 @@
     8.4 -(*  Title:      HOLCF/Tools/fixrec_package.ML
     8.5 +(*  Title:      HOLCF/Tools/fixrec.ML
     8.6      Author:     Amber Telfer and Brian Huffman
     8.7  
     8.8  Recursive function definition package for HOLCF.
     8.9  *)
    8.10  
    8.11 -signature FIXREC_PACKAGE =
    8.12 +signature FIXREC =
    8.13  sig
    8.14    val add_fixrec: bool -> (binding * typ option * mixfix) list
    8.15      -> (Attrib.binding * term) list -> local_theory -> local_theory
    8.16 @@ -16,7 +16,7 @@
    8.17    val setup: theory -> theory
    8.18  end;
    8.19  
    8.20 -structure FixrecPackage :> FIXREC_PACKAGE =
    8.21 +structure Fixrec :> FIXREC =
    8.22  struct
    8.23  
    8.24  val def_cont_fix_eq = @{thm def_cont_fix_eq};
    8.25 @@ -327,7 +327,7 @@
    8.26  (*************************************************************************)
    8.27  
    8.28  local
    8.29 -(* code adapted from HOL/Tools/primrec_package.ML *)
    8.30 +(* code adapted from HOL/Tools/primrec.ML *)
    8.31  
    8.32  fun gen_fixrec
    8.33    (set_group : bool)
     9.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 08:38:58 2009 +0200
     9.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 08:38:58 2009 +0200
     9.3 @@ -1,11 +1,11 @@
     9.4 -(*  Title:      HOLCF/Tools/pcpodef_package.ML
     9.5 +(*  Title:      HOLCF/Tools/pcpodef.ML
     9.6      Author:     Brian Huffman
     9.7  
     9.8  Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
     9.9 -typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
    9.10 +typedef (see also ~~/src/HOL/Tools/typedef.ML).
    9.11  *)
    9.12  
    9.13 -signature PCPODEF_PACKAGE =
    9.14 +signature PCPODEF =
    9.15  sig
    9.16    val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    9.17      * (binding * binding) option -> theory -> Proof.state
    9.18 @@ -17,7 +17,7 @@
    9.19      * (binding * binding) option -> theory -> Proof.state
    9.20  end;
    9.21  
    9.22 -structure PcpodefPackage :> PCPODEF_PACKAGE =
    9.23 +structure Pcpodef :> PCPODEF =
    9.24  struct
    9.25  
    9.26  (** type definitions **)