Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified proof
authorhaftmann
Fri, 23 May 2008 16:04:59 +0200
changeset 26967 27f60aaa5a7b
parent 26966 071f40487734
child 26968 bb0a56a66180
simplified proof
doc-src/IsarAdvanced/Classes/Thy/Classes.thy file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu May 22 16:34:41 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri May 23 16:04:59 2008 +0200
@@ -279,7 +279,7 @@
     instance proof
       fix n :: nat
       show "\<one> \<otimes> n = n"
-	unfolding neutral_nat_def mult_nat_def by simp
+	unfolding neutral_nat_def by simp
     next
       fix k :: int
       show "\<one> \<otimes> k = k"
isabelle