--- a/src/HOLCF/Fixrec.thy Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Fixrec.thy Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
theory Fixrec
imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec_package.ML")
+uses ("Tools/fixrec.ML")
begin
subsection {* Maybe monad type *}
@@ -599,12 +599,12 @@
subsection {* Initializing the fixrec package *}
-use "Tools/fixrec_package.ML"
+use "Tools/fixrec.ML"
-setup {* FixrecPackage.setup *}
+setup {* Fixrec.setup *}
setup {*
- FixrecPackage.add_matchers
+ Fixrec.add_matchers
[ (@{const_name up}, @{const_name match_up}),
(@{const_name sinl}, @{const_name match_sinl}),
(@{const_name sinr}, @{const_name match_sinr}),
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
theory Abstraction
imports LiveIOA
-uses ("ioa_package.ML")
+uses ("ioa.ML")
begin
defaultsort type
@@ -613,6 +613,6 @@
method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
-use "ioa_package.ML"
+use "ioa.ML"
end
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 08:38:58 2009 +0200
@@ -1,9 +1,8 @@
-(* Title: HOLCF/IOA/meta_theory/ioa_package.ML
- ID: $Id$
+(* Title: HOLCF/IOA/meta_theory/ioa.ML
Author: Tobias Hamberger, TU Muenchen
*)
-signature IOA_PACKAGE =
+signature IOA =
sig
val add_ioa: string -> string
-> (string) list -> (string) list -> (string) list
@@ -16,7 +15,7 @@
val add_rename : string -> string -> string -> theory -> theory
end;
-structure IoaPackage: IOA_PACKAGE =
+structure Ioa: IOA =
struct
val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
--- a/src/HOLCF/IsaMakefile Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/IsaMakefile Sun Jun 21 08:38:58 2009 +0200
@@ -67,8 +67,8 @@
Tools/domain/domain_library.ML \
Tools/domain/domain_syntax.ML \
Tools/domain/domain_theorems.ML \
- Tools/fixrec_package.ML \
- Tools/pcpodef_package.ML \
+ Tools/fixrec.ML \
+ Tools/pcpodef.ML \
holcf_logic.ML \
document/root.tex
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
@@ -127,7 +127,7 @@
IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
- IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
+ IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
--- a/src/HOLCF/Pcpodef.thy Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Pcpodef.thy Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
theory Pcpodef
imports Adm
-uses ("Tools/pcpodef_package.ML")
+uses ("Tools/pcpodef.ML")
begin
subsection {* Proving a subtype is a partial order *}
@@ -303,6 +303,6 @@
subsection {* HOLCF type definition package *}
-use "Tools/pcpodef_package.ML"
+use "Tools/pcpodef.ML"
end
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
signature DOMAIN_AXIOMS =
sig
- val copy_of_dtyp : (int -> term) -> DatatypeAux.dtyp -> term
+ val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
val calc_axioms :
string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
@@ -171,7 +171,7 @@
val mat_names = map mat_name con_names;
fun qualify n = Sign.full_name thy (Binding.name n);
val ms = map qualify con_names ~~ map qualify mat_names;
- in FixrecPackage.add_matchers ms thy end;
+ in Fixrec.add_matchers ms thy end;
fun add_axioms comp_dnam (eqs : eq list) thy' =
let
--- a/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Sun Jun 21 08:38:58 2009 +0200
@@ -135,10 +135,10 @@
eqtype arg;
type cons = string * arg list;
type eq = (string * typ list) * cons list;
- val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
+ val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
val is_lazy : arg -> bool;
val rec_of : arg -> int;
- val dtyp_of : arg -> DatatypeAux.dtyp;
+ val dtyp_of : arg -> Datatype.dtyp;
val sel_of : arg -> string option;
val vname : arg -> string;
val upd_vname : (string -> string) -> arg -> arg;
@@ -154,7 +154,7 @@
val idx_name : 'a list -> string -> int -> string;
val app_rec_arg : (int -> term) -> arg -> term;
val con_app : string -> arg list -> term;
- val dtyp_of_eq : eq -> DatatypeAux.dtyp;
+ val dtyp_of_eq : eq -> Datatype.dtyp;
(* Name mangling *)
@@ -215,7 +215,7 @@
(* ----- constructor list handling ----- *)
type arg =
- (bool * DatatypeAux.dtyp) * (* (lazy, recursive element) *)
+ (bool * Datatype.dtyp) * (* (lazy, recursive element) *)
string option * (* selector name *)
string; (* argument name *)
--- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 08:38:58 2009 +0200
@@ -1,10 +1,10 @@
-(* Title: HOLCF/Tools/fixrec_package.ML
+(* Title: HOLCF/Tools/fixrec.ML
Author: Amber Telfer and Brian Huffman
Recursive function definition package for HOLCF.
*)
-signature FIXREC_PACKAGE =
+signature FIXREC =
sig
val add_fixrec: bool -> (binding * typ option * mixfix) list
-> (Attrib.binding * term) list -> local_theory -> local_theory
@@ -16,7 +16,7 @@
val setup: theory -> theory
end;
-structure FixrecPackage :> FIXREC_PACKAGE =
+structure Fixrec :> FIXREC =
struct
val def_cont_fix_eq = @{thm def_cont_fix_eq};
@@ -327,7 +327,7 @@
(*************************************************************************)
local
-(* code adapted from HOL/Tools/primrec_package.ML *)
+(* code adapted from HOL/Tools/primrec.ML *)
fun gen_fixrec
(set_group : bool)
--- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 08:38:58 2009 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 08:38:58 2009 +0200
@@ -1,11 +1,11 @@
-(* Title: HOLCF/Tools/pcpodef_package.ML
+(* Title: HOLCF/Tools/pcpodef.ML
Author: Brian Huffman
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
*)
-signature PCPODEF_PACKAGE =
+signature PCPODEF =
sig
val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
* (binding * binding) option -> theory -> Proof.state
@@ -17,7 +17,7 @@
* (binding * binding) option -> theory -> Proof.state
end;
-structure PcpodefPackage :> PCPODEF_PACKAGE =
+structure Pcpodef :> PCPODEF =
struct
(** type definitions **)