author | paulson |
Fri, 21 Apr 2000 11:28:18 +0200 | |
changeset 8756 | b03a0b219139 |
parent 7702 | 35c7e0df749f |
child 9436 | 62bb04ab4b01 |
permissions | -rw-r--r-- |
(* Title: HOL/Nat.thy ID: $Id$ Author: Tobias Nipkow Copyright 1997 TU Muenchen Type "nat" is a linear order, and a datatype *) Nat = NatDef + Inductive + rep_datatype nat distinct Suc_not_Zero, Zero_not_Suc inject Suc_Suc_eq induct nat_induct instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) instance nat :: linorder (nat_le_linear) consts "^" :: ['a::power,nat] => 'a (infixr 80) end