src/HOL/Nat.thy
author paulson
Fri Sep 18 14:36:54 1998 +0200 (1998-09-18)
changeset 5499 1787c44ae4ed
parent 5188 633ec5f6c155
child 5714 b4f2e281a907
permissions -rw-r--r--
updated comments
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
setup
berghofe@5188
    12
  DatatypePackage.setup
wenzelm@4104
    13
berghofe@5188
    14
rep_datatype nat
berghofe@5188
    15
  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
berghofe@5188
    16
  inject   "[[Suc_Suc_eq]]"
berghofe@5188
    17
  induct   nat_induct
wenzelm@4104
    18
nipkow@2608
    19
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
nipkow@4640
    20
instance nat :: linorder (nat_le_linear)
oheimb@1660
    21
paulson@3370
    22
consts
paulson@3370
    23
  "^"           :: ['a::power,nat] => 'a            (infixr 80)
paulson@3370
    24
clasohm@923
    25
end