src/HOL/Finite_Set.ML
changeset 15376 302ef111b621
parent 14485 ea2707645af8
child 15392 290bc97038c7
     1.1 --- a/src/HOL/Finite_Set.ML	Mon Dec 06 07:18:24 2004 +0100
     1.2 +++ b/src/HOL/Finite_Set.ML	Mon Dec 06 14:14:03 2004 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  val foldSet_imp_finite = thm "foldSet_imp_finite";
     1.5  val fold_Un_Int = thm "ACe.fold_Un_Int";
     1.6  val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
     1.7 -val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
     1.8 +val fold_Un_disjoint2 = thm "ACe.fold_o_Un_disjoint";
     1.9  val fold_commute = thm "LC.fold_commute";
    1.10  val fold_def = thm "fold_def";
    1.11  val fold_empty = thm "fold_empty";