Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
isabelle