# HG changeset patch
# User huffman
# Date 1187632344 -7200
# Node ID 0fdabe28f0e6e1d27c9ea8c853f2da890ce425cd
# Parent  9a7a9b19e9251f9cef0bf53b9cab599a9cf754aa
remove int_of_nat; fix abs instance

diff -r 9a7a9b19e925 -r 0fdabe28f0e6 src/HOL/Library/ML_Int.thy
--- a/src/HOL/Library/ML_Int.thy	Mon Aug 20 19:51:01 2007 +0200
+++ b/src/HOL/Library/ML_Int.thy	Mon Aug 20 19:52:24 2007 +0200
@@ -109,9 +109,9 @@
   case 0 show ?case by simp
 next
   case (Suc n)
-  then have "int_of_ml_int (ml_int_of_int (int_of_nat n))
+  then have "int_of_ml_int (ml_int_of_int (int n))
     = int_of_ml_int (of_nat n)" by simp
-  then have "int_of_nat n = int_of_ml_int (of_nat n)" by simp
+  then have "int n = int_of_ml_int (of_nat n)" by simp
   then show ?case by simp
 qed
 
@@ -127,7 +127,7 @@
   "(1\<Colon>ml_int) = Numeral1"
   by simp
 
-instance ml_int :: minus
+instance ml_int :: abs
   "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..