src/HOL/Library/Nonpos_Ints.thy
changeset 62055 755fda743c49
parent 62049 b0f941e207cf
child 62072 bf3d9f113474
--- a/src/HOL/Library/Nonpos_Ints.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,15 +1,17 @@
-(*
-  Title:    HOL/Library/Nonpos_Ints.thy
-  Author:   Manuel Eberl, TU München
-  
-  The set of non-positive integers on a ring. (in analogy to the set of non-negative
-  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
+(*  Title:    HOL/Library/Nonpos_Ints.thy
+    Author:   Manuel Eberl, TU München
 *)
+
+section \<open>Non-positive integers\<close>
+
 theory Nonpos_Ints
 imports Complex_Main
 begin
 
-subsection \<open>Non-positive integers\<close>
+text \<open>
+  The set of non-positive integers on a ring. (in analogy to the set of non-negative
+  integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
+\<close>
 
 definition nonpos_Ints ("\<int>\<^sub>\<le>\<^sub>0") where "\<int>\<^sub>\<le>\<^sub>0 = {of_int n |n. n \<le> 0}"