| changeset 4477 | b3e5857d8d99 |
| parent 4423 | a129b817b58a |
| child 4686 | 74a12e86b20b |
--- a/src/HOL/Finite.ML Tue Dec 23 11:56:09 1997 +0100 +++ b/src/HOL/Finite.ML Wed Dec 24 10:02:30 1997 +0100 @@ -192,7 +192,7 @@ by (simp_tac (simpset() addsplits [expand_split]) 1); by (etac finite_imageI 1); by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1); -by (Auto_tac()); +by Auto_tac; by (rtac bexI 1); by (assume_tac 2); by (Simp_tac 1);