src/HOL/Import/HOL/divides.imp
author haftmann
Mon Feb 08 17:12:38 2010 +0100 (2010-02-08)
changeset 35050 9f841f20dca6
parent 33657 a4179bf442d1
child 44763 b50d5d694838
permissions -rw-r--r--
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 const_maps
     6   "divides" > Divides.times_class.dvd :: "nat => nat => bool"
     7 
     8 thm_maps
     9   "divides_def" > "HOL4Compat.divides_def"
    10   "ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
    11   "NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
    12   "DIVIDES_TRANS" > "Rings.dvd_trans"
    13   "DIVIDES_SUB" > "Rings.dvd_diff"
    14   "DIVIDES_REFL" > "Rings.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_antisym"
    20   "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
    21   "DIVIDES_ADD_1" > "Rings.dvd_add"
    22   "ALL_DIVIDES_0" > "Divides.dvd_0_right"
    23 
    24 end