--- a/src/HOLCF/IOA/NTP/Multiset.thy Sun Oct 21 16:27:42 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Sun Oct 21 17:48:11 2007 +0200
@@ -85,7 +85,7 @@
"!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"
apply (rule_tac M = "M" in Multiset.induction)
apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
- apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
+ apply (simp (no_asm_simp) add: neq0_conv count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
apply auto
done