src/HOL/IMP/Transition.thy
changeset 25862 9756a80d8a13
parent 23746 a455e69c31cc
child 27362 a6dc1769fdda
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue Jan 08 11:37:27 2008 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Tue Jan 08 11:37:28 2008 +0100
     1.3 @@ -189,9 +189,10 @@
     1.4  
     1.5  (*<*)
     1.6  (* FIXME: relpow.simps don't work *)
     1.7 -lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
     1.8 -lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
     1.9  lemmas [simp del] = relpow.simps
    1.10 +lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps)
    1.11 +lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps)
    1.12 +
    1.13  (*>*)
    1.14  lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
    1.15    by (cases n) auto