| changeset 4763 | 56072b72d730 |
| parent 4746 | a5dcd7e4a37d |
| child 4768 | c342d63173e9 |
--- a/src/HOL/Finite.ML Mon Mar 30 21:08:05 1998 +0200 +++ b/src/HOL/Finite.ML Mon Mar 30 21:09:46 1998 +0200 @@ -195,9 +195,7 @@ by Auto_tac; by (rtac bexI 1); by (assume_tac 2); - by (Simp_tac 1); -by (split_all_tac 1); -by (Asm_full_simp_tac 1); +by (Simp_tac 1); qed "finite_converse"; AddIffs [finite_converse];