| 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>