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
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "diffs" > "diffs_def"
     7 
     8 const_maps
     9   "diffs" > "HOL4Real.powser.diffs"
    10 
    11 thm_maps
    12   "diffs_def" > "HOL4Real.powser.diffs_def"
    13   "diffs" > "HOL4Real.powser.diffs"
    14   "TERMDIFF_LEMMA5" > "HOL4Real.powser.TERMDIFF_LEMMA5"
    15   "TERMDIFF_LEMMA4" > "HOL4Real.powser.TERMDIFF_LEMMA4"
    16   "TERMDIFF_LEMMA3" > "HOL4Real.powser.TERMDIFF_LEMMA3"
    17   "TERMDIFF_LEMMA2" > "HOL4Real.powser.TERMDIFF_LEMMA2"
    18   "TERMDIFF_LEMMA1" > "HOL4Real.powser.TERMDIFF_LEMMA1"
    19   "TERMDIFF" > "HOL4Real.powser.TERMDIFF"
    20   "POWSER_INSIDEA" > "HOL4Real.powser.POWSER_INSIDEA"
    21   "POWSER_INSIDE" > "HOL4Real.powser.POWSER_INSIDE"
    22   "POWREV" > "HOL4Real.powser.POWREV"
    23   "POWDIFF_LEMMA" > "HOL4Real.powser.POWDIFF_LEMMA"
    24   "POWDIFF" > "HOL4Real.powser.POWDIFF"
    25   "DIFFS_NEG" > "HOL4Real.powser.DIFFS_NEG"
    26   "DIFFS_LEMMA2" > "HOL4Real.powser.DIFFS_LEMMA2"
    27   "DIFFS_LEMMA" > "HOL4Real.powser.DIFFS_LEMMA"
    28   "DIFFS_EQUIV" > "HOL4Real.powser.DIFFS_EQUIV"
    29 
    30 end