# HG changeset patch
# User paulson
# Date 877078724 -7200
# Node ID 0165b805fe0925870a4c50b70da722d2ab119061
# Parent  1cc9b8ab161c5b57730e70b54d5f8d45497a953a
Better simplification eliminates a command from proof of psubset_card

diff -r 1cc9b8ab161c -r 0165b805fe09 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Oct 17 10:57:48 1997 +0200
+++ b/src/HOL/Finite.ML	Fri Oct 17 10:58:44 1997 +0200
@@ -405,7 +405,6 @@
 "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
-by (Blast_tac 1);
 by (Clarify_tac 1);
 by (case_tac "x:A" 1);
 (*1*)