author | wenzelm |
Wed, 08 Oct 2008 19:20:29 +0200 | |
changeset 28529 | 7ff939586e83 |
parent 27651 | 16a26996c30e |
child 33657 | a4179bf442d1 |
permissions | -rw-r--r-- |
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" |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
23686
diff
changeset
|
12 |
"DIVIDES_TRANS" > "Ring_and_Field.dvd_trans" |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
23686
diff
changeset
|
13 |
"DIVIDES_SUB" > "Ring_and_Field.dvd_diff" |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
23686
diff
changeset
|
14 |
"DIVIDES_REFL" > "Ring_and_Field.dvd_refl" |
14516 | 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" |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
23686
diff
changeset
|
21 |
"DIVIDES_ADD_1" > "Ring_and_Field.dvd_add" |
14516 | 22 |
"ALL_DIVIDES_0" > "Divides.dvd_0_right" |
23 |
||
24 |
end |