src/HOL/Import/HOL/divides.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17188 a26a4fc323ed
child 21416 f23e4e75dfd3
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
const_maps
skalberg@14516
     6
  "divides" > "Divides.op dvd" :: "nat => nat => bool"
skalberg@14516
     7
skalberg@14516
     8
thm_maps
skalberg@14516
     9
  "divides_def" > "HOL4Compat.divides_def"
skalberg@14516
    10
  "ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
obua@17188
    11
  "NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
skalberg@14516
    12
  "DIVIDES_TRANS" > "Divides.dvd_trans"
skalberg@14516
    13
  "DIVIDES_SUB" > "Divides.dvd_diff"
skalberg@14516
    14
  "DIVIDES_REFL" > "Divides.dvd_refl"
skalberg@14516
    15
  "DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
skalberg@14516
    16
  "DIVIDES_MULT" > "Divides.dvd_mult2"
skalberg@14516
    17
  "DIVIDES_LE" > "Divides.dvd_imp_le"
skalberg@14516
    18
  "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
skalberg@14516
    19
  "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
skalberg@14516
    20
  "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
skalberg@14516
    21
  "DIVIDES_ADD_1" > "Divides.dvd_add"
skalberg@14516
    22
  "ALL_DIVIDES_0" > "Divides.dvd_0_right"
skalberg@14516
    23
skalberg@14516
    24
end