# 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];