deleted obsolete code
authorpaulson
Mon Apr 18 10:36:05 2005 +0200 (2005-04-18)
changeset 15764250df939a1de
parent 15763 b901a127ac73
child 15765 6472d4942992
deleted obsolete code
src/ZF/Constructible/L_axioms.thy
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Apr 18 09:25:23 2005 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Mon Apr 18 10:36:05 2005 +0200
     1.3 @@ -102,90 +102,13 @@
     1.4  
     1.5  interpretation M_trivial ["L"] by (rule M_trivial_L)
     1.6  
     1.7 -(* Replaces the following code.
     1.8 -
     1.9 +(* Replaces the following declarations...
    1.10  lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
    1.11    and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
    1.12 -  and ball_iff_equiv = M_trivial.ball_iff_equiv [OF M_trivial_L]
    1.13 -  and M_equalityI = M_trivial.M_equalityI [OF M_trivial_L]
    1.14 -  and empty_abs = M_trivial.empty_abs [OF M_trivial_L]
    1.15 -  and subset_abs = M_trivial.subset_abs [OF M_trivial_L]
    1.16 -  and upair_abs = M_trivial.upair_abs [OF M_trivial_L]
    1.17 -  and upair_in_M_iff = M_trivial.upair_in_M_iff [OF M_trivial_L]
    1.18 -  and singleton_in_M_iff = M_trivial.singleton_in_M_iff [OF M_trivial_L]
    1.19 -  and pair_abs = M_trivial.pair_abs [OF M_trivial_L]
    1.20 -  and pair_in_M_iff = M_trivial.pair_in_M_iff [OF M_trivial_L]
    1.21 -  and pair_components_in_M = M_trivial.pair_components_in_M [OF M_trivial_L]
    1.22 -  and cartprod_abs = M_trivial.cartprod_abs [OF M_trivial_L]
    1.23 -  and union_abs = M_trivial.union_abs [OF M_trivial_L]
    1.24 -  and inter_abs = M_trivial.inter_abs [OF M_trivial_L]
    1.25 -  and setdiff_abs = M_trivial.setdiff_abs [OF M_trivial_L]
    1.26 -  and Union_abs = M_trivial.Union_abs [OF M_trivial_L]
    1.27 -  and Union_closed = M_trivial.Union_closed [OF M_trivial_L]
    1.28 -  and Un_closed = M_trivial.Un_closed [OF M_trivial_L]
    1.29 -  and cons_closed = M_trivial.cons_closed [OF M_trivial_L]
    1.30 -  and successor_abs = M_trivial.successor_abs [OF M_trivial_L]
    1.31 -  and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L]
    1.32 -  and separation_closed = M_trivial.separation_closed [OF M_trivial_L]
    1.33 -  and strong_replacementI = 
    1.34 -      M_trivial.strong_replacementI [OF M_trivial_L, rule_format]
    1.35 -  and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L]
    1.36 -  and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L]
    1.37 -  and lam_closed = M_trivial.lam_closed [OF M_trivial_L]
    1.38 -  and image_abs = M_trivial.image_abs [OF M_trivial_L]
    1.39 -  and powerset_Pow = M_trivial.powerset_Pow [OF M_trivial_L]
    1.40 -  and powerset_imp_subset_Pow = M_trivial.powerset_imp_subset_Pow [OF M_trivial_L]
    1.41 -  and nat_into_M = M_trivial.nat_into_M [OF M_trivial_L]
    1.42 -  and nat_case_closed = M_trivial.nat_case_closed [OF M_trivial_L]
    1.43 -  and Inl_in_M_iff = M_trivial.Inl_in_M_iff [OF M_trivial_L]
    1.44 -  and Inr_in_M_iff = M_trivial.Inr_in_M_iff [OF M_trivial_L]
    1.45 -  and lt_closed = M_trivial.lt_closed [OF M_trivial_L]
    1.46 -  and transitive_set_abs = M_trivial.transitive_set_abs [OF M_trivial_L]
    1.47 -  and ordinal_abs = M_trivial.ordinal_abs [OF M_trivial_L]
    1.48 -  and limit_ordinal_abs = M_trivial.limit_ordinal_abs [OF M_trivial_L]
    1.49 -  and successor_ordinal_abs = M_trivial.successor_ordinal_abs [OF M_trivial_L]
    1.50 -  and finite_ordinal_abs = M_trivial.finite_ordinal_abs [OF M_trivial_L]
    1.51 -  and omega_abs = M_trivial.omega_abs [OF M_trivial_L]
    1.52 -  and number1_abs = M_trivial.number1_abs [OF M_trivial_L]
    1.53 -  and number2_abs = M_trivial.number2_abs [OF M_trivial_L]
    1.54 -  and number3_abs = M_trivial.number3_abs [OF M_trivial_L]
    1.55 -
    1.56 +...
    1.57  declare rall_abs [simp]
    1.58  declare rex_abs [simp]
    1.59 -declare empty_abs [simp]
    1.60 -declare subset_abs [simp]
    1.61 -declare upair_abs [simp]
    1.62 -declare upair_in_M_iff [iff]
    1.63 -declare singleton_in_M_iff [iff]
    1.64 -declare pair_abs [simp]
    1.65 -declare pair_in_M_iff [iff]
    1.66 -declare cartprod_abs [simp]
    1.67 -declare union_abs [simp]
    1.68 -declare inter_abs [simp]
    1.69 -declare setdiff_abs [simp]
    1.70 -declare Union_abs [simp]
    1.71 -declare Union_closed [intro, simp]
    1.72 -declare Un_closed [intro, simp]
    1.73 -declare cons_closed [intro, simp]
    1.74 -declare successor_abs [simp]
    1.75 -declare succ_in_M_iff [iff]
    1.76 -declare separation_closed [intro, simp]
    1.77 -declare strong_replacement_closed [intro, simp]
    1.78 -declare RepFun_closed [intro, simp]
    1.79 -declare lam_closed [intro, simp]
    1.80 -declare image_abs [simp]
    1.81 -declare nat_into_M [intro]
    1.82 -declare Inl_in_M_iff [iff]
    1.83 -declare Inr_in_M_iff [iff]
    1.84 -declare transitive_set_abs [simp]
    1.85 -declare ordinal_abs [simp]
    1.86 -declare limit_ordinal_abs [simp]
    1.87 -declare successor_ordinal_abs [simp]
    1.88 -declare finite_ordinal_abs [simp]
    1.89 -declare omega_abs [simp]
    1.90 -declare number1_abs [simp]
    1.91 -declare number2_abs [simp]
    1.92 -declare number3_abs [simp]
    1.93 +...and dozens of similar ones.
    1.94  *)
    1.95  
    1.96  subsection{*Instantiation of the locale @{text reflection}*}
    1.97 @@ -332,8 +255,7 @@
    1.98       "[| REFLECTS[P,Q]; Ord(i);
    1.99           !!j. [|i<j;  \<forall>x \<in> Lset(j). P(x) <-> Q(j,x)|] ==> R |]
   1.100        ==> R"
   1.101 -apply (drule ReflectsD, assumption, blast)
   1.102 -done
   1.103 +by (drule ReflectsD, assumption, blast)
   1.104  
   1.105  lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B"
   1.106  by blast