src/ZF/Epsilon.thy
changeset 46751 6b94c39b7366
parent 45602 2a858377c3d2
child 46820 c656222c4dc1
     1.1 --- a/src/ZF/Epsilon.thy	Thu Mar 01 14:48:32 2012 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Thu Mar 01 17:13:54 2012 +0000
     1.3 @@ -396,58 +396,4 @@
     1.4       ==> rec(n,a,b) : C(n)"
     1.5  by (erule nat_induct, auto)
     1.6  
     1.7 -ML
     1.8 -{*
     1.9 -val arg_subset_eclose = @{thm arg_subset_eclose};
    1.10 -val arg_into_eclose = @{thm arg_into_eclose};
    1.11 -val Transset_eclose = @{thm Transset_eclose};
    1.12 -val eclose_subset = @{thm eclose_subset};
    1.13 -val ecloseD = @{thm ecloseD};
    1.14 -val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
    1.15 -val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
    1.16 -val eclose_induct = @{thm eclose_induct};
    1.17 -val eps_induct = @{thm eps_induct};
    1.18 -val eclose_least = @{thm eclose_least};
    1.19 -val eclose_induct_down = @{thm eclose_induct_down};
    1.20 -val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
    1.21 -val mem_eclose_trans = @{thm mem_eclose_trans};
    1.22 -val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
    1.23 -val under_Memrel = @{thm under_Memrel};
    1.24 -val under_Memrel_eclose = @{thm under_Memrel_eclose};
    1.25 -val wfrec_ssubst = @{thm wfrec_ssubst};
    1.26 -val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
    1.27 -val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
    1.28 -val transrec = @{thm transrec};
    1.29 -val def_transrec = @{thm def_transrec};
    1.30 -val transrec_type = @{thm transrec_type};
    1.31 -val eclose_sing_Ord = @{thm eclose_sing_Ord};
    1.32 -val Ord_transrec_type = @{thm Ord_transrec_type};
    1.33 -val rank = @{thm rank};
    1.34 -val Ord_rank = @{thm Ord_rank};
    1.35 -val rank_of_Ord = @{thm rank_of_Ord};
    1.36 -val rank_lt = @{thm rank_lt};
    1.37 -val eclose_rank_lt = @{thm eclose_rank_lt};
    1.38 -val rank_mono = @{thm rank_mono};
    1.39 -val rank_Pow = @{thm rank_Pow};
    1.40 -val rank_0 = @{thm rank_0};
    1.41 -val rank_succ = @{thm rank_succ};
    1.42 -val rank_Union = @{thm rank_Union};
    1.43 -val rank_eclose = @{thm rank_eclose};
    1.44 -val rank_pair1 = @{thm rank_pair1};
    1.45 -val rank_pair2 = @{thm rank_pair2};
    1.46 -val the_equality_if = @{thm the_equality_if};
    1.47 -val rank_apply = @{thm rank_apply};
    1.48 -val mem_eclose_subset = @{thm mem_eclose_subset};
    1.49 -val eclose_mono = @{thm eclose_mono};
    1.50 -val eclose_idem = @{thm eclose_idem};
    1.51 -val transrec2_0 = @{thm transrec2_0};
    1.52 -val transrec2_succ = @{thm transrec2_succ};
    1.53 -val transrec2_Limit = @{thm transrec2_Limit};
    1.54 -val recursor_0 = @{thm recursor_0};
    1.55 -val recursor_succ = @{thm recursor_succ};
    1.56 -val rec_0 = @{thm rec_0};
    1.57 -val rec_succ = @{thm rec_succ};
    1.58 -val rec_type = @{thm rec_type};
    1.59 -*}
    1.60 -
    1.61  end