changeset 5562 | 02261e6880d1 |
child 5582 | a356fb49e69e |
5561:426c1e330903 | 5562:02261e6880d1 |
---|---|
1 (* Title: Integ/Int.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Type "int" is a linear order |
|
7 *) |
|
8 |
|
9 Int = IntDef + |
|
10 |
|
11 instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) |
|
12 instance int :: linorder (zle_linear) |
|
13 |
|
14 constdefs |
|
15 nat :: int => nat |
|
16 "nat(Z) == if neg Z then 0 else (@ m. Z = $# m)" |
|
17 |
|
18 end |