author | nipkow |
Sat, 08 Oct 2005 15:20:58 +0200 | |
changeset 17790 | aa6ec0efe4d3 |
parent 17789 | ccba4e900023 |
child 17791 | f4453001cbde |
--- a/src/HOLCF/IOA/NTP/Multiset.ML Fri Oct 07 23:29:00 2005 +0200 +++ b/src/HOLCF/IOA/NTP/Multiset.ML Sat Oct 08 15:20:58 2005 +0200 @@ -68,7 +68,7 @@ by (asm_simp_tac (simpset() addsimps [count_addm_simp,Multiset.delm_nonempty_def, Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1); - by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1); + by (Auto_tac); qed "countm_done_delm";