# HG changeset patch
# User huffman
# Date 1266426538 28800
# Node ID 31cbcb0190035c8b12006525ae3e657de39066a7
# Parent  07b3112e464b527693c69ecf2ec3132c4e563bf6
fix warnings about duplicate simp rules

diff -r 07b3112e464b -r 31cbcb019003 src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 08:19:46 2010 -0800
+++ b/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 09:08:58 2010 -0800
@@ -56,10 +56,10 @@
 lemma wir_moel: "YS = YYS"
   apply (rule stream.take_lemmas)
   apply (induct_tac n)
-  apply (simp (no_asm) add: stream.rews)
+  apply (simp (no_asm))
   apply (subst YS_def2)
   apply (subst YYS_def2)
-  apply (simp add: stream.rews)
+  apply simp
   apply (rule lemma5 [symmetric, THEN subst])
   apply (rule refl)
   done
diff -r 07b3112e464b -r 31cbcb019003 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Wed Feb 17 08:19:46 2010 -0800
+++ b/src/HOLCF/ex/Dnat.thy	Wed Feb 17 09:08:58 2010 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Dnat.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 
 Theory for the domain of natural numbers  dnat = one ++ dnat
@@ -34,18 +33,18 @@
 
 lemma iterator1: "iterator $ UU $ f $ x = UU"
   apply (subst iterator_def2)
-  apply (simp add: dnat.rews)
+  apply simp
   done
 
 lemma iterator2: "iterator $ dzero $ f $ x = x"
   apply (subst iterator_def2)
-  apply (simp add: dnat.rews)
+  apply simp
   done
 
 lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
   apply (rule trans)
    apply (subst iterator_def2)
-   apply (simp add: dnat.rews)
+   apply simp
   apply (rule refl)
   done
 
@@ -59,13 +58,13 @@
    apply (rule_tac x = y in dnat.casedist)
      apply simp
     apply simp
-   apply (simp add: dnat.dist_les)
+   apply simp
   apply (rule allI)
   apply (rule_tac x = y in dnat.casedist)
     apply (fast intro!: UU_I)
    apply (thin_tac "ALL y. d << y --> d = UU | d = y")
-   apply (simp add: dnat.dist_les)
-  apply (simp (no_asm_simp) add: dnat.rews dnat.injects dnat.inverts)
+   apply simp
+  apply (simp (no_asm_simp))
   apply (drule_tac x="da" in spec)
   apply simp
   done
diff -r 07b3112e464b -r 31cbcb019003 src/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOLCF/ex/Powerdomain_ex.thy	Wed Feb 17 08:19:46 2010 -0800
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Wed Feb 17 09:08:58 2010 -0800
@@ -14,8 +14,6 @@
 
 domain ordering = LT | EQ | GT
 
-declare ordering.rews [simp]
-
 definition
   compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
   "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
diff -r 07b3112e464b -r 31cbcb019003 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed Feb 17 08:19:46 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Wed Feb 17 09:08:58 2010 -0800
@@ -54,8 +54,6 @@
                         | \<infinity>    \<Rightarrow> s1)"
 
 
-declare stream.rews [simp add]
-
 (* ----------------------------------------------------------------------- *)
 (* theorems about scons                                                    *)
 (* ----------------------------------------------------------------------- *)
@@ -149,13 +147,13 @@
 apply (insert stream.reach [of s], erule subst) back
 apply (simp add: fix_def2 stream.take_def)
 apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
-by (simp add: chain_iterate)
+by simp
 
 lemma chain_stream_take: "chain (%i. stream_take i$s)"
 apply (rule chainI)
 apply (rule monofun_cfun_fun)
 apply (simp add: stream.take_def del: iterate_Suc)
-by (rule chainE, simp add: chain_iterate)
+by (rule chainE, simp)
 
 lemma stream_take_prefix [simp]: "stream_take n$s << s"
 apply (insert stream_reach2 [of s])