src/HOL/Nat.thy
changeset 64712 38adf0c59c35
parent 64447 e44f5c123f26
child 64849 766db3539859
equal deleted inserted replaced
64711:45dfaad6d852 64712:38adf0c59c35
     1 (*  Title:      HOL/Nat.thy
     1 (*  Title:      HOL/Nat.thy
     2     Author:     Tobias Nipkow
     2     Author:     Tobias Nipkow
     3     Author:     Lawrence C Paulson
     3     Author:     Lawrence C Paulson
     4     Author:     Markus Wenzel
     4     Author:     Markus Wenzel
     5 
       
     6 Type "nat" is a linear order, and a datatype; arithmetic operators + -
       
     7 and * (for div and mod, see theory Divides).
       
     8 *)
     5 *)
     9 
     6 
    10 section \<open>Natural numbers\<close>
     7 section \<open>Natural numbers\<close>
    11 
     8 
    12 theory Nat
     9 theory Nat