--- a/src/HOL/Library/Extended.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Extended.thy Tue Nov 19 10:05:53 2013 +0100
@@ -161,8 +161,8 @@
apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
done
-lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
-by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
+lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
+by (simp only: Fin_numeral uminus_extended.simps[symmetric])
instantiation extended :: (lattice)bounded_lattice