# HG changeset patch # User haftmann # Date 1204054694 -3600 # Node ID 6094349a4de92ab873322bf8b844e1eb6641bb5b # Parent cbe6f8af8db2ee7afeecb53c6f63bcd238a5c245 tuned heading diff -r cbe6f8af8db2 -r 6094349a4de9 src/HOL/Nat.thy --- 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