author | haftmann |
Fri, 30 Dec 2016 18:02:27 +0100 | |
changeset 64712 | 38adf0c59c35 |
parent 64711 | 45dfaad6d852 |
child 64713 | 9638c07283bc |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.thy Fri Dec 30 20:43:40 2016 +0100 +++ b/src/HOL/Nat.thy Fri Dec 30 18:02:27 2016 +0100 @@ -2,9 +2,6 @@ Author: Tobias Nipkow Author: Lawrence C Paulson Author: Markus Wenzel - -Type "nat" is a linear order, and a datatype; arithmetic operators + - -and * (for div and mod, see theory Divides). *) section \<open>Natural numbers\<close>