--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 07:22:30 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Mar 08 07:37:11 2010 -0800
@@ -16,9 +16,7 @@
abs_inverse : thm,
rep_inverse : thm
}
-
- val define_take_functions :
- (binding * iso_info) list -> theory ->
+ type take_info =
{ take_consts : term list,
take_defs : thm list,
chain_take_thms : thm list,
@@ -27,7 +25,9 @@
deflation_take_thms : thm list,
finite_consts : term list,
finite_defs : thm list
- } * theory
+ }
+ val define_take_functions :
+ (binding * iso_info) list -> theory -> take_info * theory
val map_of_typ :
theory -> (typ * term) list -> typ -> term
@@ -52,6 +52,17 @@
rep_inverse : thm
};
+type take_info =
+ { take_consts : term list,
+ take_defs : thm list,
+ chain_take_thms : thm list,
+ take_0_thms : thm list,
+ take_Suc_thms : thm list,
+ deflation_take_thms : thm list,
+ finite_consts : term list,
+ finite_defs : thm list
+ };
+
val beta_ss =
HOL_basic_ss
addsimps simp_thms