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/NSA/StarDef.thy
changeset 61076 bdc1e2f0a86a
parent 60867 86e7560e07d0
child 61275 053ec04ea866 
--- a/src/HOL/NSA/StarDef.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -927,7 +927,7 @@
     then show ?case by simp
   next
     case (Suc n)
-    have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
+    have "\<And>x::'a star. x * ( *f* (\<lambda>x::'a. x ^ n)) x = ( *f* (\<lambda>x::'a. x * x ^ n)) x"
       by transfer simp
     with Suc show ?case by simp
   qed
isabelle