|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
const_maps
|
|
23686
|
6 |
"divides" > Divides.times_class.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
|