src/HOL/Import/HOL/divides.imp
author haftmann
Sat, 18 Nov 2006 00:20:24 +0100
changeset 21416 f23e4e75dfd3
parent 17188 a26a4fc323ed
child 23686 9d5671f61b31
permissions -rw-r--r--
dvd_def now with object equality
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
import
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
const_maps
21416
f23e4e75dfd3 dvd_def now with object equality
haftmann
parents: 17188
diff changeset
     6
  "divides" > "Divides.dvd" :: "nat => nat => bool"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "divides_def" > "HOL4Compat.divides_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "ONE_DIVIDES_ALL" > "HOL4Base.divides.ONE_DIVIDES_ALL"
17188
a26a4fc323ed Updated import.
obua
parents: 14516
diff changeset
    11
  "NOT_LT_DIV" > "NatSimprocs.nat_dvd_not_less"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  "DIVIDES_TRANS" > "Divides.dvd_trans"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "DIVIDES_SUB" > "Divides.dvd_diff"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "DIVIDES_REFL" > "Divides.dvd_refl"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  "DIVIDES_MULT_LEFT" > "HOL4Base.divides.DIVIDES_MULT_LEFT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
  "DIVIDES_MULT" > "Divides.dvd_mult2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
  "DIVIDES_LE" > "Divides.dvd_imp_le"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "DIVIDES_ADD_1" > "Divides.dvd_add"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  "ALL_DIVIDES_0" > "Divides.dvd_0_right"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
end