--- a/src/HOL/Nat.thy Tue Feb 26 20:38:13 2008 +0100+++ b/src/HOL/Nat.thy Tue Feb 26 20:38:14 2008 +0100@@ -1149,7 +1149,7 @@ by (auto simp add: expand_fun_eq)-subsection {*The Set of Natural Numbers*}+subsection {* The Set of Natural Numbers *} context semiring_1 begin