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.
stabilized proof of card_mono
authoroheimb
Fri, 11 Sep 1998 14:09:46 +0200
changeset 5477 41ab0f44dd8f
parent 5476 1c09934fe445
child 5478 33fcf0e60547
stabilized proof of card_mono
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite.ML	Fri Sep 11 12:55:40 1998 +0200
+++ b/src/HOL/Finite.ML	Fri Sep 11 14:09:46 1998 +0200
@@ -327,7 +327,8 @@
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
 by (fast_tac (claset() addss
-	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
+	      (simpset() addsimps [subset_insert_iff, finite_subset]
+			 delsimps [insert_subset])) 1);
 qed_spec_mp "card_mono";
isabelle