summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Power.thy

changeset 63040 | eb4ddd18d635 |

parent 62481 | b5d8e57826df |

child 63417 | c184ec919c70 |

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