Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
constant dvd now in class target
authorhaftmann
Tue, 10 Jul 2007 09:23:12 +0200
changeset 23686 9d5671f61b31
parent 23685 1b0f4071946c
child 23687 06884f7ffb18
constant dvd now in class target
src/HOL/Import/Generate-HOL/GenHOL4Base.thy file | annotate | diff | comparison | revisions
src/HOL/Import/HOL/divides.imp file | annotate | diff | comparison | revisions 
--- 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;
 
--- 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"
isabelle