summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Power.thy

changeset 63040 | eb4ddd18d635 |

parent 62481 | b5d8e57826df |

child 63417 | c184ec919c70 |

--- a/src/HOL/Power.thy Sun Apr 24 21:31:14 2016 +0200 +++ b/src/HOL/Power.thy Mon Apr 25 16:09:26 2016 +0200 @@ -90,7 +90,7 @@ case 0 then show ?case by (simp add: fun_eq_iff) next case (Suc n) - def g \<equiv> "\<lambda>x. f x - 1" + define g where "g x = f x - 1" for x with Suc have "n = g x" by simp with Suc have "times x ^^ g x = times (x ^ g x)" by simp moreover from Suc g_def have "f x = g x + 1" by simp