14516

1 
import


2 


3 
import_segment "hol4"


4 


5 
const_maps

21416

6 
"divides" > "Divides.dvd" :: "nat => nat => bool"

14516

7 


8 
thm_maps


9 
"divides_def" > "HOL4Compat.divides_def"


10 
"ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"

17188

11 
"NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"

14516

12 
"DIVIDES_TRANS" > "Divides.dvd_trans"


13 
"DIVIDES_SUB" > "Divides.dvd_diff"


14 
"DIVIDES_REFL" > "Divides.dvd_refl"


15 
"DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"


16 
"DIVIDES_MULT" > "Divides.dvd_mult2"


17 
"DIVIDES_LE" > "Divides.dvd_imp_le"


18 
"DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"


19 
"DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"


20 
"DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"


21 
"DIVIDES_ADD_1" > "Divides.dvd_add"


22 
"ALL_DIVIDES_0" > "Divides.dvd_0_right"


23 


24 
end
