# HG changeset patch
# User haftmann
# Date 1184052192 -7200
# Node ID 9d5671f61b3154b89cc277389af4b505569595f9
# Parent  1b0f4071946c495b89684b9bd169debd14c83d7a
constant dvd now in class target

diff -r 1b0f4071946c -r 9d5671f61b31 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:11 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Tue Jul 10 09:23:12 2007 +0200
@@ -208,7 +208,7 @@
 import_theory divides;
 
 const_maps
-    divides > "Divides.dvd" :: "[nat,nat]=>bool";
+  divides > Divides.times_class.dvd :: "[nat,nat]=>bool";
 
 end_import;
 
diff -r 1b0f4071946c -r 9d5671f61b31 src/HOL/Import/HOL/divides.imp
--- a/src/HOL/Import/HOL/divides.imp	Tue Jul 10 09:23:11 2007 +0200
+++ b/src/HOL/Import/HOL/divides.imp	Tue Jul 10 09:23:12 2007 +0200
@@ -3,7 +3,7 @@
 import_segment "hol4"
 
 const_maps
-  "divides" > "Divides.dvd" :: "nat => nat => bool"
+  "divides" > Divides.times_class.dvd :: "nat => nat => bool"
 
 thm_maps
   "divides_def" > "HOL4Compat.divides_def"