src/HOL/Nat.thy
author wenzelm
Mon Oct 04 21:44:28 1999 +0200 (1999-10-04)
changeset 7702 35c7e0df749f
parent 5714 b4f2e281a907
child 9436 62bb04ab4b01
permissions -rw-r--r--
removed DatatypePackage.setup;
clasohm@923
     1
(*  Title:      HOL/Nat.thy
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
paulson@5499
     6
Type "nat" is a linear order, and a datatype
clasohm@923
     7
*)
clasohm@923
     8
berghofe@5188
     9
Nat = NatDef + Inductive +
clasohm@923
    10
berghofe@5188
    11
rep_datatype nat
berghofe@5714
    12
  distinct Suc_not_Zero, Zero_not_Suc
berghofe@5714
    13
  inject   Suc_Suc_eq
berghofe@5188
    14
  induct   nat_induct
wenzelm@4104
    15
nipkow@2608
    16
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
nipkow@4640
    17
instance nat :: linorder (nat_le_linear)
oheimb@1660
    18
paulson@3370
    19
consts
paulson@3370
    20
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
paulson@3370
    21
clasohm@923
    22
end