src/HOL/Finite_Set.ML
changeset 12693 827818b891c7
parent 12396 2298d5b8e530
child 14485 ea2707645af8
     1.1 --- a/src/HOL/Finite_Set.ML	Wed Jan 09 17:56:46 2002 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Jan 10 01:10:58 2002 +0100
     1.3 @@ -97,18 +97,18 @@
     1.4  val finite_subset = thm "finite_subset";
     1.5  val finite_subset_induct = thm "finite_subset_induct";
     1.6  val finite_trancl = thm "finite_trancl";
     1.7 -val foldSet_determ = thm "foldSet_determ";
     1.8 +val foldSet_determ = thm "LC.foldSet_determ";
     1.9  val foldSet_imp_finite = thm "foldSet_imp_finite";
    1.10 -val fold_Un_Int = thm "fold_Un_Int";
    1.11 -val fold_Un_disjoint = thm "fold_Un_disjoint";
    1.12 -val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
    1.13 -val fold_commute = thm "fold_commute";
    1.14 +val fold_Un_Int = thm "ACe.fold_Un_Int";
    1.15 +val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    1.16 +val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
    1.17 +val fold_commute = thm "LC.fold_commute";
    1.18  val fold_def = thm "fold_def";
    1.19  val fold_empty = thm "fold_empty";
    1.20 -val fold_equality = thm "fold_equality";
    1.21 -val fold_insert = thm "fold_insert";
    1.22 -val fold_nest_Un_Int = thm "fold_nest_Un_Int";
    1.23 -val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
    1.24 +val fold_equality = thm "LC.fold_equality";
    1.25 +val fold_insert = thm "LC.fold_insert";
    1.26 +val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
    1.27 +val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
    1.28  val n_sub_lemma = thm "n_sub_lemma";
    1.29  val n_subsets = thm "n_subsets";
    1.30  val psubset_card_mono = thm "psubset_card_mono";