src/HOL/Import/HOL/divides.imp
changeset 14516 a183dec876ab
child 17188 a26a4fc323ed
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOL/divides.imp	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,24 @@
     1.4 +import
     1.5 +
     1.6 +import_segment "hol4"
     1.7 +
     1.8 +const_maps
     1.9 +  "divides" > "Divides.op dvd" :: "nat => nat => bool"
    1.10 +
    1.11 +thm_maps
    1.12 +  "divides_def" > "HOL4Compat.divides_def"
    1.13 +  "ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
    1.14 +  "NOT_LT_DIV" > "HOL4Base.divides.NOT_LT_DIV"
    1.15 +  "DIVIDES_TRANS" > "Divides.dvd_trans"
    1.16 +  "DIVIDES_SUB" > "Divides.dvd_diff"
    1.17 +  "DIVIDES_REFL" > "Divides.dvd_refl"
    1.18 +  "DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
    1.19 +  "DIVIDES_MULT" > "Divides.dvd_mult2"
    1.20 +  "DIVIDES_LE" > "Divides.dvd_imp_le"
    1.21 +  "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
    1.22 +  "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
    1.23 +  "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
    1.24 +  "DIVIDES_ADD_1" > "Divides.dvd_add"
    1.25 +  "ALL_DIVIDES_0" > "Divides.dvd_0_right"
    1.26 +
    1.27 +end