src/ZF/Constructible/Rec_Separation.thy
changeset 15766 b08feb003f3c
parent 13807 a28a8fbc76d4
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Mon Apr 18 15:53:51 2005 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Mon Apr 18 15:54:23 2005 +0200
     1.3 @@ -184,11 +184,7 @@
     1.4  by (rule M_trancl.intro
     1.5           [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
     1.6  
     1.7 -lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
     1.8 -  and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
     1.9 -  and trans_wfrec_abs = M_trancl.trans_wfrec_abs [OF M_trancl_L]
    1.10 -  and eq_pair_wfrec_iff = M_trancl.eq_pair_wfrec_iff [OF M_trancl_L]
    1.11 -
    1.12 +interpretation M_trancl [L] by (rule M_trancl_axioms_L)
    1.13  
    1.14  
    1.15  subsection{*@{term L} is Closed Under the Operator @{term list}*}
    1.16 @@ -374,17 +370,7 @@
    1.17   apply (rule M_datatypes_axioms_L) 
    1.18   done
    1.19  
    1.20 -lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
    1.21 -  and formula_closed = M_datatypes.formula_closed [OF M_datatypes_L]
    1.22 -  and list_abs = M_datatypes.list_abs [OF M_datatypes_L]
    1.23 -  and formula_abs = M_datatypes.formula_abs [OF M_datatypes_L]
    1.24 -  and nth_abs = M_datatypes.nth_abs [OF M_datatypes_L]
    1.25 -
    1.26 -declare list_closed [intro,simp]
    1.27 -declare formula_closed [intro,simp]
    1.28 -declare list_abs [simp]
    1.29 -declare formula_abs [simp]
    1.30 -declare nth_abs [simp]
    1.31 +interpretation M_datatypes [L] by (rule M_datatypes_axioms_L)
    1.32  
    1.33  
    1.34  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
    1.35 @@ -447,8 +433,7 @@
    1.36    apply (rule M_eclose_axioms_L)
    1.37    done
    1.38  
    1.39 -lemmas eclose_closed [intro, simp] = M_eclose.eclose_closed [OF M_eclose_L]
    1.40 -  and eclose_abs [intro, simp] = M_eclose.eclose_abs [OF M_eclose_L]
    1.41 -  and transrec_replacementI = M_eclose.transrec_replacementI [OF M_eclose_L]
    1.42 +interpretation M_eclose [L] by (rule M_eclose_axioms_L)
    1.43 +
    1.44  
    1.45  end