src/HOL/Nat.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5714 b4f2e281a907
child 7702 35c7e0df749f
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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@5714
    15
  distinct Suc_not_Zero, Zero_not_Suc
berghofe@5714
    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