# HG changeset patch
# User haftmann
# Date 1206738061 -3600
# Node ID 5d6b3a8081312658240985ab27a4ff012ac510bb
# Parent  1f55aef1390374057af9ddc646cff86968ac58fd
accomodated to sledgehammer theory dependency requirement

diff -r 1f55aef13903 -r 5d6b3a808131 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Mar 28 22:00:59 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Fri Mar 28 22:01:01 2008 +0100
@@ -6,7 +6,7 @@
 header {* Pretty integer literals for code generation *}
 
 theory Code_Integer
-imports Presburger
+imports ATP_Linkup
 begin
 
 text {*