src/ZF/Constructible/Separation.thy
changeset 13429 2232810416fc
parent 13428 99e52e78eb65
child 13437 01b3fc0cc1b8
     1.1 --- a/src/ZF/Constructible/Separation.thy	Mon Jul 29 00:57:16 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Separation.thy	Mon Jul 29 18:07:53 2002 +0200
     1.3 @@ -448,7 +448,9 @@
     1.4  text{*Separation (and Strong Replacement) for basic set-theoretic constructions
     1.5  such as intersection, Cartesian Product and image.*}
     1.6  
     1.7 -theorem M_axioms_axioms_L: "M_axioms_axioms(L)"
     1.8 +theorem M_axioms_L: "PROP M_axioms(L)"
     1.9 +  apply (rule M_axioms.intro)
    1.10 +   apply (rule M_triv_axioms_L)
    1.11    apply (rule M_axioms_axioms.intro)
    1.12                 apply (assumption | rule
    1.13                   Inter_separation cartprod_separation image_separation
    1.14 @@ -458,12 +460,6 @@
    1.15                   obase_separation obase_equals_separation
    1.16                   omap_replacement is_recfun_separation)+
    1.17    done
    1.18 -  
    1.19 -theorem M_axioms_L: "PROP M_axioms(L)"
    1.20 -  apply (rule M_axioms.intro)
    1.21 -   apply (rule M_triv_axioms_L)
    1.22 -  apply (rule M_axioms_axioms_L)
    1.23 -  done
    1.24  
    1.25  lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
    1.26    and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
    1.27 @@ -570,35 +566,34 @@
    1.28    and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
    1.29    and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
    1.30  
    1.31 -
    1.32 -declare cartprod_closed [intro,simp]
    1.33 -declare sum_closed [intro,simp]
    1.34 -declare converse_closed [intro,simp]
    1.35 +declare cartprod_closed [intro, simp]
    1.36 +declare sum_closed [intro, simp]
    1.37 +declare converse_closed [intro, simp]
    1.38  declare converse_abs [simp]
    1.39 -declare image_closed [intro,simp]
    1.40 +declare image_closed [intro, simp]
    1.41  declare vimage_abs [simp]
    1.42 -declare vimage_closed [intro,simp]
    1.43 +declare vimage_closed [intro, simp]
    1.44  declare domain_abs [simp]
    1.45 -declare domain_closed [intro,simp]
    1.46 +declare domain_closed [intro, simp]
    1.47  declare range_abs [simp]
    1.48 -declare range_closed [intro,simp]
    1.49 +declare range_closed [intro, simp]
    1.50  declare field_abs [simp]
    1.51 -declare field_closed [intro,simp]
    1.52 +declare field_closed [intro, simp]
    1.53  declare relation_abs [simp]
    1.54  declare function_abs [simp]
    1.55 -declare apply_closed [intro,simp]
    1.56 +declare apply_closed [intro, simp]
    1.57  declare typed_function_abs [simp]
    1.58  declare injection_abs [simp]
    1.59  declare surjection_abs [simp]
    1.60  declare bijection_abs [simp]
    1.61 -declare comp_closed [intro,simp]
    1.62 +declare comp_closed [intro, simp]
    1.63  declare composition_abs [simp]
    1.64  declare restriction_abs [simp]
    1.65 -declare restrict_closed [intro,simp]
    1.66 +declare restrict_closed [intro, simp]
    1.67  declare Inter_abs [simp]
    1.68 -declare Inter_closed [intro,simp]
    1.69 -declare Int_closed [intro,simp]
    1.70 +declare Inter_closed [intro, simp]
    1.71 +declare Int_closed [intro, simp]
    1.72  declare is_funspace_abs [simp]
    1.73 -declare finite_funspace_closed [intro,simp]
    1.74 +declare finite_funspace_closed [intro, simp]
    1.75  
    1.76  end