src/HOLCF/IOA/NTP/Multiset.ML
changeset 17790 aa6ec0efe4d3
parent 17244 0b2ff9541727
equal deleted inserted replaced
17789:ccba4e900023 17790:aa6ec0efe4d3
    66                           [Multiset.delm_empty_def,
    66                           [Multiset.delm_empty_def,
    67                            Multiset.countm_empty_def]) 1);
    67                            Multiset.countm_empty_def]) 1);
    68   by (asm_simp_tac (simpset() addsimps 
    68   by (asm_simp_tac (simpset() addsimps 
    69                       [count_addm_simp,Multiset.delm_nonempty_def,
    69                       [count_addm_simp,Multiset.delm_nonempty_def,
    70                        Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
    70                        Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
    71   by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    71   by (Auto_tac);
    72 qed "countm_done_delm";
    72 qed "countm_done_delm";
    73 
    73 
    74 
    74 
    75 Addsimps [count_addm_simp, count_delm_simp,
    75 Addsimps [count_addm_simp, count_delm_simp,
    76           Multiset.countm_empty_def, Multiset.delm_empty_def,
    76           Multiset.countm_empty_def, Multiset.delm_empty_def,