--- 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
--- 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
--- 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)"
--- 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])