src/HOL/Integ/Int.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Int.thy	Fri Sep 25 13:57:01 1998 +0200
@@ -0,0 +1,18 @@
+(*  Title:      Integ/Int.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Type "int" is a linear order
+*)
+
+Int = IntDef +
+
+instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
+instance int :: linorder (zle_linear)
+
+constdefs
+  nat  :: int => nat
+  "nat(Z) == if neg Z then 0 else (@ m. Z = $# m)"
+
+end