14516
|
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
|