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