1.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 08:19:46 2010 -0800
     1.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Wed Feb 17 09:08:58 2010 -0800
     1.3 @@ -56,10 +56,10 @@
     1.4  lemma wir_moel: "YS = YYS"
     1.5    apply (rule stream.take_lemmas)
     1.6    apply (induct_tac n)
     1.7 -  apply (simp (no_asm) add: stream.rews)
     1.8 +  apply (simp (no_asm))
     1.9    apply (subst YS_def2)
    1.10    apply (subst YYS_def2)
    1.11 -  apply (simp add: stream.rews)
    1.12 +  apply simp
    1.13    apply (rule lemma5 [symmetric, THEN subst])
    1.14    apply (rule refl)
    1.15    done

     2.1 --- a/src/HOLCF/ex/Dnat.thy	Wed Feb 17 08:19:46 2010 -0800
     2.2 +++ b/src/HOLCF/ex/Dnat.thy	Wed Feb 17 09:08:58 2010 -0800
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOLCF/Dnat.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Franz Regensburger
     2.7  
     2.8  Theory for the domain of natural numbers  dnat = one ++ dnat
     2.9 @@ -34,18 +33,18 @@
    2.10  
    2.11  lemma iterator1: "iterator $ UU $ f $ x = UU"
    2.12    apply (subst iterator_def2)
    2.13 -  apply (simp add: dnat.rews)
    2.14 +  apply simp
    2.15    done
    2.16  
    2.17  lemma iterator2: "iterator $ dzero $ f $ x = x"
    2.18    apply (subst iterator_def2)
    2.19 -  apply (simp add: dnat.rews)
    2.20 +  apply simp
    2.21    done
    2.22  
    2.23  lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
    2.24    apply (rule trans)
    2.25     apply (subst iterator_def2)
    2.26 -   apply (simp add: dnat.rews)
    2.27 +   apply simp
    2.28    apply (rule refl)
    2.29    done
    2.30  
    2.31 @@ -59,13 +58,13 @@
    2.32     apply (rule_tac x = y in dnat.casedist)
    2.33       apply simp
    2.34      apply simp
    2.35 -   apply (simp add: dnat.dist_les)
    2.36 +   apply simp
    2.37    apply (rule allI)
    2.38    apply (rule_tac x = y in dnat.casedist)
    2.39      apply (fast intro!: UU_I)
    2.40     apply (thin_tac "ALL y. d << y --> d = UU | d = y")
    2.41 -   apply (simp add: dnat.dist_les)
    2.42 -  apply (simp (no_asm_simp) add: dnat.rews dnat.injects dnat.inverts)
    2.43 +   apply simp
    2.44 +  apply (simp (no_asm_simp))
    2.45    apply (drule_tac x="da" in spec)
    2.46    apply simp
    2.47    done

     3.1 --- a/src/HOLCF/ex/Powerdomain_ex.thy	Wed Feb 17 08:19:46 2010 -0800
     3.2 +++ b/src/HOLCF/ex/Powerdomain_ex.thy	Wed Feb 17 09:08:58 2010 -0800
     3.3 @@ -14,8 +14,6 @@
     3.4  
     3.5  domain ordering = LT | EQ | GT
     3.6  
     3.7 -declare ordering.rews [simp]
     3.8 -
     3.9  definition
    3.10    compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
    3.11    "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"

     4.1 --- a/src/HOLCF/ex/Stream.thy	Wed Feb 17 08:19:46 2010 -0800
     4.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Feb 17 09:08:58 2010 -0800
     4.3 @@ -54,8 +54,6 @@
     4.4                          | \<infinity>    \<Rightarrow> s1)"
     4.5  
     4.6  
     4.7 -declare stream.rews [simp add]
     4.8 -
     4.9  (* ----------------------------------------------------------------------- *)
    4.10  (* theorems about scons                                                    *)
    4.11  (* ----------------------------------------------------------------------- *)
    4.12 @@ -149,13 +147,13 @@
    4.13  apply (insert stream.reach [of s], erule subst) back
    4.14  apply (simp add: fix_def2 stream.take_def)
    4.15  apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
    4.16 -by (simp add: chain_iterate)
    4.17 +by simp
    4.18  
    4.19  lemma chain_stream_take: "chain (%i. stream_take i$s)"
    4.20  apply (rule chainI)
    4.21  apply (rule monofun_cfun_fun)
    4.22  apply (simp add: stream.take_def del: iterate_Suc)
    4.23 -by (rule chainE, simp add: chain_iterate)
    4.24 +by (rule chainE, simp)
    4.25  
    4.26  lemma stream_take_prefix [simp]: "stream_take n$s << s"
    4.27  apply (insert stream_reach2 [of s])