# HG changeset patch
# User oheimb
# Date 891284986 -7200
# Node ID 56072b72d7309b701d64370b41bc191600b10e5f
# Parent  afebaa81f14881ad3ac6d9d8f5da5ee1bc59e264
adapted proof of finite_converse

diff -r afebaa81f148 -r 56072b72d730 src/HOL/Finite.ML
--- 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];