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.
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
changeset 26967 27f60aaa5a7b
parent 25871 45753d56d935
child 27065 f68aa7b5a0f3 
--- 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