# HG changeset patch # User oheimb # Date 905515786 -7200 # Node ID 41ab0f44dd8f70ba95454e025efc2d630a214108 # Parent 1c09934fe445a1841d32e4432026128954b1200f stabilized proof of card_mono diff -r 1c09934fe445 -r 41ab0f44dd8f src/HOL/Finite.ML --- 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";