Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better simplification eliminates a command from proof of psubset_card
authorpaulson
Fri, 17 Oct 1997 10:58:44 +0200
changeset 3911 0165b805fe09
parent 3910 1cc9b8ab161c
child 3912 4ed64ad7fb42
Better simplification eliminates a command from proof of psubset_card
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- 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*)
isabelle