Cleaned up, now use interpretation.

--- a/src/ZF/Constructible/Rec_Separation.thy	Mon Apr 18 15:53:51 2005 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Apr 18 15:54:23 2005 +0200
@@ -184,11 +184,7 @@
 by (rule M_trancl.intro
          [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
 
-lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
-  and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
-  and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
-  and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
-
+interpretation M_trancl [L] by (rule M_trancl_axioms_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*}
@@ -374,17 +370,7 @@
  apply (rule M_datatypes_axioms_L) 
  done
 
-lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
-  and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
-  and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
-  and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L]
-  and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L]
-
-declare list_closed [intro,simp]
-declare formula_closed [intro,simp]
-declare list_abs [simp]
-declare formula_abs [simp]
-declare nth_abs [simp]
+interpretation M_datatypes [L] by (rule M_datatypes_axioms_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
@@ -447,8 +433,7 @@
   apply (rule M_eclose_axioms_L)
   done
 
-lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
-  and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
-  and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
+interpretation M_eclose [L] by (rule M_eclose_axioms_L)
+
 
 end

--- a/src/ZF/Constructible/Separation.thy	Mon Apr 18 15:53:51 2005 +0200
+++ b/src/ZF/Constructible/Separation.thy	Mon Apr 18 15:54:23 2005 +0200
@@ -305,113 +305,7 @@
 theorem M_basic_L: "PROP M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
-
-lemmas cartprod_iff = M_basic.cartprod_iff [OF M_basic_L]
-  and cartprod_closed = M_basic.cartprod_closed [OF M_basic_L]
-  and sum_closed = M_basic.sum_closed [OF M_basic_L]
-  and M_converse_iff = M_basic.M_converse_iff [OF M_basic_L]
-  and converse_closed = M_basic.converse_closed [OF M_basic_L]
-  and converse_abs = M_basic.converse_abs [OF M_basic_L]
-  and image_closed = M_basic.image_closed [OF M_basic_L]
-  and vimage_abs = M_basic.vimage_abs [OF M_basic_L]
-  and vimage_closed = M_basic.vimage_closed [OF M_basic_L]
-  and domain_abs = M_basic.domain_abs [OF M_basic_L]
-  and domain_closed = M_basic.domain_closed [OF M_basic_L]
-  and range_abs = M_basic.range_abs [OF M_basic_L]
-  and range_closed = M_basic.range_closed [OF M_basic_L]
-  and field_abs = M_basic.field_abs [OF M_basic_L]
-  and field_closed = M_basic.field_closed [OF M_basic_L]
-  and relation_abs = M_basic.relation_abs [OF M_basic_L]
-  and function_abs = M_basic.function_abs [OF M_basic_L]
-  and apply_closed = M_basic.apply_closed [OF M_basic_L]
-  and apply_abs = M_basic.apply_abs [OF M_basic_L]
-  and typed_function_abs = M_basic.typed_function_abs [OF M_basic_L]
-  and injection_abs = M_basic.injection_abs [OF M_basic_L]
-  and surjection_abs = M_basic.surjection_abs [OF M_basic_L]
-  and bijection_abs = M_basic.bijection_abs [OF M_basic_L]
-  and M_comp_iff = M_basic.M_comp_iff [OF M_basic_L]
-  and comp_closed = M_basic.comp_closed [OF M_basic_L]
-  and composition_abs = M_basic.composition_abs [OF M_basic_L]
-  and restriction_is_function = M_basic.restriction_is_function [OF M_basic_L]
-  and restriction_abs = M_basic.restriction_abs [OF M_basic_L]
-  and M_restrict_iff = M_basic.M_restrict_iff [OF M_basic_L]
-  and restrict_closed = M_basic.restrict_closed [OF M_basic_L]
-  and Inter_abs = M_basic.Inter_abs [OF M_basic_L]
-  and Inter_closed = M_basic.Inter_closed [OF M_basic_L]
-  and Int_closed = M_basic.Int_closed [OF M_basic_L]
-  and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L]
-  and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L]
-  and funspace_succ = M_basic.funspace_succ [OF M_basic_L]
-  and finite_funspace_closed = M_basic.finite_funspace_closed [OF M_basic_L]
+interpretation M_basic [L] by (rule M_basic_axioms_L)
 
-lemmas is_recfun_equal = M_basic.is_recfun_equal [OF M_basic_L]
-  and is_recfun_cut = M_basic.is_recfun_cut [OF M_basic_L]
-  and is_recfun_functional = M_basic.is_recfun_functional [OF M_basic_L]
-  and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L]
-  and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L]
-  and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L]
-  and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L]
-  and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L]
-  and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L]
-  and irreflexive_abs = M_basic.irreflexive_abs [OF M_basic_L]
-  and transitive_rel_abs = M_basic.transitive_rel_abs [OF M_basic_L]
-  and linear_rel_abs = M_basic.linear_rel_abs [OF M_basic_L]
-  and wellordered_is_trans_on = M_basic.wellordered_is_trans_on [OF M_basic_L]
-  and wellordered_is_linear = M_basic.wellordered_is_linear [OF M_basic_L]
-  and wellordered_is_wellfounded_on = M_basic.wellordered_is_wellfounded_on [OF M_basic_L]
-  and wellfounded_imp_wellfounded_on = M_basic.wellfounded_imp_wellfounded_on [OF M_basic_L]
-  and wellfounded_on_subset_A = M_basic.wellfounded_on_subset_A [OF M_basic_L]
-  and wellfounded_on_iff_wellfounded = M_basic.wellfounded_on_iff_wellfounded [OF M_basic_L]
-  and wellfounded_on_imp_wellfounded = M_basic.wellfounded_on_imp_wellfounded [OF M_basic_L]
-  and wellfounded_on_field_imp_wellfounded = M_basic.wellfounded_on_field_imp_wellfounded [OF M_basic_L]
-  and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L]
-  and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L]
-  and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L]
-  and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L]
-  and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L]
-  and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L]
-  and wf_imp_relativized = M_basic.wf_imp_relativized [OF M_basic_L]
-  and well_ord_imp_relativized = M_basic.well_ord_imp_relativized [OF M_basic_L]
-  and order_isomorphism_abs = M_basic.order_isomorphism_abs [OF M_basic_L]
-  and pred_set_abs = M_basic.pred_set_abs [OF M_basic_L]
-
-lemmas pred_closed = M_basic.pred_closed [OF M_basic_L]
-  and membership_abs = M_basic.membership_abs [OF M_basic_L]
-  and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L]
-  and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L]
-  and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L]
-  and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L]
-
-declare cartprod_closed [intro, simp]
-declare sum_closed [intro, simp]
-declare converse_closed [intro, simp]
-declare converse_abs [simp]
-declare image_closed [intro, simp]
-declare vimage_abs [simp]
-declare vimage_closed [intro, simp]
-declare domain_abs [simp]
-declare domain_closed [intro, simp]
-declare range_abs [simp]
-declare range_closed [intro, simp]
-declare field_abs [simp]
-declare field_closed [intro, simp]
-declare relation_abs [simp]
-declare function_abs [simp]
-declare apply_closed [intro, simp]
-declare typed_function_abs [simp]
-declare injection_abs [simp]
-declare surjection_abs [simp]
-declare bijection_abs [simp]
-declare comp_closed [intro, simp]
-declare composition_abs [simp]
-declare restriction_abs [simp]
-declare restrict_closed [intro, simp]
-declare Inter_abs [simp]
-declare Inter_closed [intro, simp]
-declare Int_closed [intro, simp]
-declare is_funspace_abs [simp]
-declare finite_funspace_closed [intro, simp]
-declare membership_abs [simp] 
-declare Memrel_closed  [intro,simp]
 
 end