# HG changeset patch
# User haftmann
# Date 1211551499 -7200
# Node ID 27f60aaa5a7bb7512094f5dd322976200aa696f4
# Parent  071f40487734ba9885e936d69a02e0b7acc12e5b
simplified proof

diff -r 071f40487734 -r 27f60aaa5a7b doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- 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"