--- a/src/ZF/Epsilon.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/ZF/Epsilon.thy Mon Sep 06 19:13:10 2010 +0200
@@ -398,56 +398,56 @@
ML
{*
-val arg_subset_eclose = thm "arg_subset_eclose";
-val arg_into_eclose = thm "arg_into_eclose";
-val Transset_eclose = thm "Transset_eclose";
-val eclose_subset = thm "eclose_subset";
-val ecloseD = thm "ecloseD";
-val arg_in_eclose_sing = thm "arg_in_eclose_sing";
-val arg_into_eclose_sing = thm "arg_into_eclose_sing";
-val eclose_induct = thm "eclose_induct";
-val eps_induct = thm "eps_induct";
-val eclose_least = thm "eclose_least";
-val eclose_induct_down = thm "eclose_induct_down";
-val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
-val mem_eclose_trans = thm "mem_eclose_trans";
-val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
-val under_Memrel = thm "under_Memrel";
-val under_Memrel_eclose = thm "under_Memrel_eclose";
-val wfrec_ssubst = thm "wfrec_ssubst";
-val wfrec_eclose_eq = thm "wfrec_eclose_eq";
-val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
-val transrec = thm "transrec";
-val def_transrec = thm "def_transrec";
-val transrec_type = thm "transrec_type";
-val eclose_sing_Ord = thm "eclose_sing_Ord";
-val Ord_transrec_type = thm "Ord_transrec_type";
-val rank = thm "rank";
-val Ord_rank = thm "Ord_rank";
-val rank_of_Ord = thm "rank_of_Ord";
-val rank_lt = thm "rank_lt";
-val eclose_rank_lt = thm "eclose_rank_lt";
-val rank_mono = thm "rank_mono";
-val rank_Pow = thm "rank_Pow";
-val rank_0 = thm "rank_0";
-val rank_succ = thm "rank_succ";
-val rank_Union = thm "rank_Union";
-val rank_eclose = thm "rank_eclose";
-val rank_pair1 = thm "rank_pair1";
-val rank_pair2 = thm "rank_pair2";
-val the_equality_if = thm "the_equality_if";
-val rank_apply = thm "rank_apply";
-val mem_eclose_subset = thm "mem_eclose_subset";
-val eclose_mono = thm "eclose_mono";
-val eclose_idem = thm "eclose_idem";
-val transrec2_0 = thm "transrec2_0";
-val transrec2_succ = thm "transrec2_succ";
-val transrec2_Limit = thm "transrec2_Limit";
-val recursor_0 = thm "recursor_0";
-val recursor_succ = thm "recursor_succ";
-val rec_0 = thm "rec_0";
-val rec_succ = thm "rec_succ";
-val rec_type = thm "rec_type";
+val arg_subset_eclose = @{thm arg_subset_eclose};
+val arg_into_eclose = @{thm arg_into_eclose};
+val Transset_eclose = @{thm Transset_eclose};
+val eclose_subset = @{thm eclose_subset};
+val ecloseD = @{thm ecloseD};
+val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
+val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
+val eclose_induct = @{thm eclose_induct};
+val eps_induct = @{thm eps_induct};
+val eclose_least = @{thm eclose_least};
+val eclose_induct_down = @{thm eclose_induct_down};
+val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
+val mem_eclose_trans = @{thm mem_eclose_trans};
+val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
+val under_Memrel = @{thm under_Memrel};
+val under_Memrel_eclose = @{thm under_Memrel_eclose};
+val wfrec_ssubst = @{thm wfrec_ssubst};
+val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
+val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
+val transrec = @{thm transrec};
+val def_transrec = @{thm def_transrec};
+val transrec_type = @{thm transrec_type};
+val eclose_sing_Ord = @{thm eclose_sing_Ord};
+val Ord_transrec_type = @{thm Ord_transrec_type};
+val rank = @{thm rank};
+val Ord_rank = @{thm Ord_rank};
+val rank_of_Ord = @{thm rank_of_Ord};
+val rank_lt = @{thm rank_lt};
+val eclose_rank_lt = @{thm eclose_rank_lt};
+val rank_mono = @{thm rank_mono};
+val rank_Pow = @{thm rank_Pow};
+val rank_0 = @{thm rank_0};
+val rank_succ = @{thm rank_succ};
+val rank_Union = @{thm rank_Union};
+val rank_eclose = @{thm rank_eclose};
+val rank_pair1 = @{thm rank_pair1};
+val rank_pair2 = @{thm rank_pair2};
+val the_equality_if = @{thm the_equality_if};
+val rank_apply = @{thm rank_apply};
+val mem_eclose_subset = @{thm mem_eclose_subset};
+val eclose_mono = @{thm eclose_mono};
+val eclose_idem = @{thm eclose_idem};
+val transrec2_0 = @{thm transrec2_0};
+val transrec2_succ = @{thm transrec2_succ};
+val transrec2_Limit = @{thm transrec2_Limit};
+val recursor_0 = @{thm recursor_0};
+val recursor_succ = @{thm recursor_succ};
+val rec_0 = @{thm rec_0};
+val rec_succ = @{thm rec_succ};
+val rec_type = @{thm rec_type};
*}
end