src/ZF/Epsilon.thy
changeset 39159 0dec18004e75
parent 35762 af3ff2ba4c54
child 45602 2a858377c3d2
     1.1 --- a/src/ZF/Epsilon.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -398,56 +398,56 @@
     1.4  
     1.5  ML
     1.6  {*
     1.7 -val arg_subset_eclose = thm "arg_subset_eclose";
     1.8 -val arg_into_eclose = thm "arg_into_eclose";
     1.9 -val Transset_eclose = thm "Transset_eclose";
    1.10 -val eclose_subset = thm "eclose_subset";
    1.11 -val ecloseD = thm "ecloseD";
    1.12 -val arg_in_eclose_sing = thm "arg_in_eclose_sing";
    1.13 -val arg_into_eclose_sing = thm "arg_into_eclose_sing";
    1.14 -val eclose_induct = thm "eclose_induct";
    1.15 -val eps_induct = thm "eps_induct";
    1.16 -val eclose_least = thm "eclose_least";
    1.17 -val eclose_induct_down = thm "eclose_induct_down";
    1.18 -val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
    1.19 -val mem_eclose_trans = thm "mem_eclose_trans";
    1.20 -val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
    1.21 -val under_Memrel = thm "under_Memrel";
    1.22 -val under_Memrel_eclose = thm "under_Memrel_eclose";
    1.23 -val wfrec_ssubst = thm "wfrec_ssubst";
    1.24 -val wfrec_eclose_eq = thm "wfrec_eclose_eq";
    1.25 -val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
    1.26 -val transrec = thm "transrec";
    1.27 -val def_transrec = thm "def_transrec";
    1.28 -val transrec_type = thm "transrec_type";
    1.29 -val eclose_sing_Ord = thm "eclose_sing_Ord";
    1.30 -val Ord_transrec_type = thm "Ord_transrec_type";
    1.31 -val rank = thm "rank";
    1.32 -val Ord_rank = thm "Ord_rank";
    1.33 -val rank_of_Ord = thm "rank_of_Ord";
    1.34 -val rank_lt = thm "rank_lt";
    1.35 -val eclose_rank_lt = thm "eclose_rank_lt";
    1.36 -val rank_mono = thm "rank_mono";
    1.37 -val rank_Pow = thm "rank_Pow";
    1.38 -val rank_0 = thm "rank_0";
    1.39 -val rank_succ = thm "rank_succ";
    1.40 -val rank_Union = thm "rank_Union";
    1.41 -val rank_eclose = thm "rank_eclose";
    1.42 -val rank_pair1 = thm "rank_pair1";
    1.43 -val rank_pair2 = thm "rank_pair2";
    1.44 -val the_equality_if = thm "the_equality_if";
    1.45 -val rank_apply = thm "rank_apply";
    1.46 -val mem_eclose_subset = thm "mem_eclose_subset";
    1.47 -val eclose_mono = thm "eclose_mono";
    1.48 -val eclose_idem = thm "eclose_idem";
    1.49 -val transrec2_0 = thm "transrec2_0";
    1.50 -val transrec2_succ = thm "transrec2_succ";
    1.51 -val transrec2_Limit = thm "transrec2_Limit";
    1.52 -val recursor_0 = thm "recursor_0";
    1.53 -val recursor_succ = thm "recursor_succ";
    1.54 -val rec_0 = thm "rec_0";
    1.55 -val rec_succ = thm "rec_succ";
    1.56 -val rec_type = thm "rec_type";
    1.57 +val arg_subset_eclose = @{thm arg_subset_eclose};
    1.58 +val arg_into_eclose = @{thm arg_into_eclose};
    1.59 +val Transset_eclose = @{thm Transset_eclose};
    1.60 +val eclose_subset = @{thm eclose_subset};
    1.61 +val ecloseD = @{thm ecloseD};
    1.62 +val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
    1.63 +val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
    1.64 +val eclose_induct = @{thm eclose_induct};
    1.65 +val eps_induct = @{thm eps_induct};
    1.66 +val eclose_least = @{thm eclose_least};
    1.67 +val eclose_induct_down = @{thm eclose_induct_down};
    1.68 +val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
    1.69 +val mem_eclose_trans = @{thm mem_eclose_trans};
    1.70 +val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
    1.71 +val under_Memrel = @{thm under_Memrel};
    1.72 +val under_Memrel_eclose = @{thm under_Memrel_eclose};
    1.73 +val wfrec_ssubst = @{thm wfrec_ssubst};
    1.74 +val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
    1.75 +val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
    1.76 +val transrec = @{thm transrec};
    1.77 +val def_transrec = @{thm def_transrec};
    1.78 +val transrec_type = @{thm transrec_type};
    1.79 +val eclose_sing_Ord = @{thm eclose_sing_Ord};
    1.80 +val Ord_transrec_type = @{thm Ord_transrec_type};
    1.81 +val rank = @{thm rank};
    1.82 +val Ord_rank = @{thm Ord_rank};
    1.83 +val rank_of_Ord = @{thm rank_of_Ord};
    1.84 +val rank_lt = @{thm rank_lt};
    1.85 +val eclose_rank_lt = @{thm eclose_rank_lt};
    1.86 +val rank_mono = @{thm rank_mono};
    1.87 +val rank_Pow = @{thm rank_Pow};
    1.88 +val rank_0 = @{thm rank_0};
    1.89 +val rank_succ = @{thm rank_succ};
    1.90 +val rank_Union = @{thm rank_Union};
    1.91 +val rank_eclose = @{thm rank_eclose};
    1.92 +val rank_pair1 = @{thm rank_pair1};
    1.93 +val rank_pair2 = @{thm rank_pair2};
    1.94 +val the_equality_if = @{thm the_equality_if};
    1.95 +val rank_apply = @{thm rank_apply};
    1.96 +val mem_eclose_subset = @{thm mem_eclose_subset};
    1.97 +val eclose_mono = @{thm eclose_mono};
    1.98 +val eclose_idem = @{thm eclose_idem};
    1.99 +val transrec2_0 = @{thm transrec2_0};
   1.100 +val transrec2_succ = @{thm transrec2_succ};
   1.101 +val transrec2_Limit = @{thm transrec2_Limit};
   1.102 +val recursor_0 = @{thm recursor_0};
   1.103 +val recursor_succ = @{thm recursor_succ};
   1.104 +val rec_0 = @{thm rec_0};
   1.105 +val rec_succ = @{thm rec_succ};
   1.106 +val rec_type = @{thm rec_type};
   1.107  *}
   1.108  
   1.109  end