# HG changeset patch
# User nipkow
# Date 1193172505 -7200
# Node ID aa847439803022b7743d0e025a2fe5aa6701a679
# Parent  72fcf0832cfe7fbe6750a69897bf57966fa4e7a4
changed back from ~=0 to >0

diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Tue Oct 23 14:00:06 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Tue Oct 23 22:48:25 2007 +0200
@@ -168,7 +168,7 @@
 apply (rule impI)
 apply (erule conjE)+
 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
-  Multiset.delm_nonempty_def neq0_conv split add: split_if)
+  Multiset.delm_nonempty_def split add: split_if)
 apply (rule allI)
 apply (rule conjI)
 apply (rule impI)
diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOLCF/IOA/NTP/Multiset.thy	Tue Oct 23 14:00:06 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy	Tue Oct 23 22:48:25 2007 +0200
@@ -75,17 +75,17 @@
   done
 
 
-lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P \<noteq> 0"
+lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P > 0"
   apply (rule_tac M = "M" in Multiset.induction)
   apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def)
-  apply (simp (no_asm_simp) add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
+  apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
   done
 
 lemma countm_done_delm: 
    "!!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: neq0_conv count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
+  apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
   apply auto
   done
 
diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue Oct 23 14:00:06 2007 +0200
+++ b/src/HOLCF/IsaMakefile	Tue Oct 23 22:48:25 2007 +0200
@@ -34,7 +34,7 @@
   Tools/domain/domain_extender.ML Tools/domain/domain_axioms.ML			\
   Tools/domain/domain_library.ML Tools/domain/domain_syntax.ML			\
   Tools/domain/domain_theorems.ML Tools/fixrec_package.ML			\
-  Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex ex/Stream.thy	\
+  Tools/pcpodef_package.ML Tr.thy Up.thy document/root.tex	\
   holcf_logic.ML
 	@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
 
@@ -52,7 +52,7 @@
 
 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 
-$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.thy \
+$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
   ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
   ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
diff -r 72fcf0832cfe -r aa8474398030 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Tue Oct 23 14:00:06 2007 +0200
+++ b/src/HOLCF/ex/Stream.thy	Tue Oct 23 22:48:25 2007 +0200
@@ -693,8 +693,7 @@
 lemma take_i_rt_prefix_lemma:
 "[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2"
 apply (case_tac "n=0",simp)
-apply (insert neq0_conv [of n])
-apply (insert not0_implies_Suc [of n],auto)
+apply (auto)
 apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 &
                     i_rt 0 s1 << i_rt 0 s2")
  defer 1