| changeset 3382 | 8db8fc8607d9 |
| parent 3368 | be517d000c02 |
| child 3389 | 3150eba724a1 |
--- a/src/HOL/Finite.ML Mon Jun 02 12:12:27 1997 +0200 +++ b/src/HOL/Finite.ML Mon Jun 02 12:12:57 1997 +0200 @@ -62,7 +62,7 @@ goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)"; by (stac insert_is_Un 1); -by (Simp_tac 1); +by (simp_tac (HOL_ss addsimps [subset_Fin]) 1); by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1); qed "insert_Fin"; Addsimps[insert_Fin];