src/HOL/Import/HOL/powser.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
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
def_maps
skalberg@14516
     6
  "diffs" > "diffs_def"
skalberg@14516
     7
skalberg@14516
     8
const_maps
skalberg@14516
     9
  "diffs" > "HOL4Real.powser.diffs"
skalberg@14516
    10
skalberg@14516
    11
thm_maps
skalberg@14516
    12
  "diffs_def" > "HOL4Real.powser.diffs_def"
skalberg@14516
    13
  "diffs" > "HOL4Real.powser.diffs"
skalberg@14516
    14
  "TERMDIFF_LEMMA5" > "HOL4Real.powser.TERMDIFF_LEMMA5"
skalberg@14516
    15
  "TERMDIFF_LEMMA4" > "HOL4Real.powser.TERMDIFF_LEMMA4"
skalberg@14516
    16
  "TERMDIFF_LEMMA3" > "HOL4Real.powser.TERMDIFF_LEMMA3"
skalberg@14516
    17
  "TERMDIFF_LEMMA2" > "HOL4Real.powser.TERMDIFF_LEMMA2"
skalberg@14516
    18
  "TERMDIFF_LEMMA1" > "HOL4Real.powser.TERMDIFF_LEMMA1"
skalberg@14516
    19
  "TERMDIFF" > "HOL4Real.powser.TERMDIFF"
skalberg@14516
    20
  "POWSER_INSIDEA" > "HOL4Real.powser.POWSER_INSIDEA"
skalberg@14516
    21
  "POWSER_INSIDE" > "HOL4Real.powser.POWSER_INSIDE"
skalberg@14516
    22
  "POWREV" > "HOL4Real.powser.POWREV"
skalberg@14516
    23
  "POWDIFF_LEMMA" > "HOL4Real.powser.POWDIFF_LEMMA"
skalberg@14516
    24
  "POWDIFF" > "HOL4Real.powser.POWDIFF"
skalberg@14516
    25
  "DIFFS_NEG" > "HOL4Real.powser.DIFFS_NEG"
skalberg@14516
    26
  "DIFFS_LEMMA2" > "HOL4Real.powser.DIFFS_LEMMA2"
skalberg@14516
    27
  "DIFFS_LEMMA" > "HOL4Real.powser.DIFFS_LEMMA"
skalberg@14516
    28
  "DIFFS_EQUIV" > "HOL4Real.powser.DIFFS_EQUIV"
skalberg@14516
    29
skalberg@14516
    30
end