author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Wed, 07 Sep 2011 07:59:45 +0900 | |
changeset 44763 | b50d5d694838 |
parent 35050 | 9f841f20dca6 |
permissions | -rw-r--r-- |
14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
const_maps |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
6 |
"divides" > "Rings.dvd_class.dvd" :: "nat => nat => bool" |
14516 | 7 |
|
8 |
thm_maps |
|
9 |
"divides_def" > "HOL4Compat.divides_def" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
10 |
"ONE_DIVIDES_ALL" > "GCD.gcd_lcm_complete_lattice_nat.bot_least" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
11 |
"NOT_LT_DIV" > "Nat.nat_dvd_not_less" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
12 |
"DIVIDES_TRANS" > "Nat.dvd.order_trans" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
13 |
"DIVIDES_SUB" > "Nat.dvd_diff_nat" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
14 |
"DIVIDES_REFL" > "Nat.dvd.order_refl" |
14516 | 15 |
"DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
16 |
"DIVIDES_MULT" > "Rings.comm_semiring_1_class.dvd_mult2" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
17 |
"DIVIDES_LE" > "Nat.dvd_imp_le" |
14516 | 18 |
"DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT" |
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
19 |
"DIVIDES_ANTISYM" > "Nat.dvd.antisym" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
20 |
"DIVIDES_ADD_2" > "Primes.divides_add_revr" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
21 |
"DIVIDES_ADD_1" > "Rings.comm_semiring_1_class.dvd_add" |
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35050
diff
changeset
|
22 |
"ALL_DIVIDES_0" > "GCD.gcd_lcm_complete_lattice_nat.top_greatest" |
14516 | 23 |
|
24 |
end |