changeset 21416 | f23e4e75dfd3 |
parent 17188 | a26a4fc323ed |
child 23686 | 9d5671f61b31 |
--- a/src/HOL/Import/HOL/divides.imp Sat Nov 18 00:20:22 2006 +0100 +++ b/src/HOL/Import/HOL/divides.imp Sat Nov 18 00:20:24 2006 +0100 @@ -3,7 +3,7 @@ import_segment "hol4" const_maps - "divides" > "Divides.op dvd" :: "nat => nat => bool" + "divides" > "Divides.dvd" :: "nat => nat => bool" thm_maps "divides_def" > "HOL4Compat.divides_def"