src/HOL/Relation_Power.thy
changeset 30079 293b896b9c25
parent 29654 24e73987bfe2
child 30949 37f887b55e7f
     1.1 --- a/src/HOL/Relation_Power.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/Relation_Power.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -61,16 +61,16 @@
     1.4  
     1.5  lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
     1.6  proof -
     1.7 -  have "f((f^n) x) = (f^(n+1)) x" by simp
     1.8 +  have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
     1.9    also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
    1.10 -  also have "\<dots> = (f^n)(f x)" by simp
    1.11 +  also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
    1.12    finally show ?thesis .
    1.13  qed
    1.14  
    1.15  lemma rel_pow_1 [simp]:
    1.16    fixes R :: "('a*'a)set"
    1.17    shows "R^1 = R"
    1.18 -  by simp
    1.19 +  unfolding One_nat_def by simp
    1.20  
    1.21  lemma rel_pow_0_I: "(x,x) : R^0"
    1.22    by simp