# HG changeset patch
# User haftmann
# Date 1199788648 -3600
# Node ID 9756a80d8a136542ecec1d3ece41c864209fa45d
# Parent  494d9301cc751273ab3e4f9b76a37c99c7168f91
tuned

diff -r 494d9301cc75 -r 9756a80d8a13 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue Jan 08 11:37:27 2008 +0100
+++ b/src/HOL/IMP/Transition.thy	Tue Jan 08 11:37:28 2008 +0100
@@ -189,9 +189,10 @@
 
 (*<*)
 (* FIXME: relpow.simps don't work *)
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
 lemmas [simp del] = relpow.simps
+lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps)
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps)
+
 (*>*)
 lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   by (cases n) auto