# HG changeset patch
# User nipkow
# Date 1032933127 -7200
# Node ID 87cf22cdb8056dfa05b24d640549aec522c6240c
# Parent  ecb6ecd9af130236c55ae4fff5907149557d9ce0
converted to Isar

diff -r ecb6ecd9af13 -r 87cf22cdb805 src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Wed Sep 25 07:42:24 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  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
-*)
-
-theory Int = IntDef
-files ("int.ML"):
-
-instance int :: order
-proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
-
-instance int :: plus_ac0
-proof qed (rule zadd_commute zadd_assoc zadd_0)+
-
-instance int :: linorder
-proof qed (rule zle_linear)
-
-constdefs
-  nat  :: "int => nat"
- "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
-
-defs (overloaded)
-  zabs_def:  "abs(i::int) == if i < 0 then -i else i"
-
-use "int.ML"
-
-end