equal
deleted
inserted
replaced
166 apply (tactic "tac 1") |
166 apply (tactic "tac 1") |
167 apply (tactic "tac_ren 1") |
167 apply (tactic "tac_ren 1") |
168 apply (rule impI) |
168 apply (rule impI) |
169 apply (erule conjE)+ |
169 apply (erule conjE)+ |
170 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def |
170 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def |
171 Multiset.delm_nonempty_def split add: split_if) |
171 Multiset.delm_nonempty_def neq0_conv split add: split_if) |
172 apply (rule allI) |
172 apply (rule allI) |
173 apply (rule conjI) |
173 apply (rule conjI) |
174 apply (rule impI) |
174 apply (rule impI) |
175 apply hypsubst |
175 apply hypsubst |
176 apply (rule pred_suc [THEN iffD1]) |
176 apply (rule pred_suc [THEN iffD1]) |