|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"transitive" > "transitive_primdef"
|
|
|
7 |
"the_fun" > "the_fun_primdef"
|
|
|
8 |
"pred_reflexive" > "pred_reflexive_def"
|
|
|
9 |
"inv_image" > "inv_image_primdef"
|
|
|
10 |
"approx" > "approx_primdef"
|
|
|
11 |
"WFREC" > "WFREC_def"
|
|
|
12 |
"WF" > "WF_def"
|
|
|
13 |
"TC" > "TC_def"
|
|
|
14 |
"RTC" > "RTC_def"
|
|
|
15 |
"RESTRICT" > "RESTRICT_def"
|
|
|
16 |
"RC" > "RC_primdef"
|
|
|
17 |
"EMPTY_REL" > "EMPTY_REL_def"
|
|
|
18 |
|
|
|
19 |
const_maps
|
|
|
20 |
"transitive" > "HOL4Base.relation.transitive"
|
|
|
21 |
"the_fun" > "HOL4Base.relation.the_fun"
|
|
|
22 |
"pred_reflexive" > "HOL4Base.relation.pred_reflexive"
|
|
|
23 |
"inv_image" > "HOL4Base.relation.inv_image"
|
|
|
24 |
"approx" > "HOL4Base.relation.approx"
|
|
|
25 |
"WFREC" > "HOL4Base.relation.WFREC"
|
|
|
26 |
"WF" > "HOL4Base.relation.WF"
|
|
|
27 |
"TC" > "HOL4Base.relation.TC"
|
|
|
28 |
"RTC" > "HOL4Base.relation.RTC"
|
|
|
29 |
"RESTRICT" > "HOL4Base.relation.RESTRICT"
|
|
|
30 |
"RC" > "HOL4Base.relation.RC"
|
|
|
31 |
"EMPTY_REL" > "HOL4Base.relation.EMPTY_REL"
|
|
|
32 |
|
|
|
33 |
const_renames
|
|
|
34 |
"reflexive" > "pred_reflexive"
|
|
|
35 |
|
|
|
36 |
thm_maps
|
|
|
37 |
"transitive_primdef" > "HOL4Base.relation.transitive_primdef"
|
|
|
38 |
"transitive_def" > "HOL4Base.relation.transitive_def"
|
|
|
39 |
"the_fun_primdef" > "HOL4Base.relation.the_fun_primdef"
|
|
|
40 |
"the_fun_def" > "HOL4Base.relation.the_fun_def"
|
|
|
41 |
"reflexive_def" > "HOL4Base.relation.reflexive_def"
|
|
|
42 |
"pred_reflexive_def" > "HOL4Base.relation.pred_reflexive_def"
|
|
|
43 |
"inv_image_primdef" > "HOL4Base.relation.inv_image_primdef"
|
|
|
44 |
"inv_image_def" > "HOL4Base.relation.inv_image_def"
|
|
|
45 |
"approx_primdef" > "HOL4Base.relation.approx_primdef"
|
|
|
46 |
"approx_def" > "HOL4Base.relation.approx_def"
|
|
|
47 |
"WF_inv_image" > "HOL4Base.relation.WF_inv_image"
|
|
|
48 |
"WF_def" > "HOL4Base.relation.WF_def"
|
|
|
49 |
"WF_TC" > "HOL4Base.relation.WF_TC"
|
|
|
50 |
"WF_SUBSET" > "HOL4Base.relation.WF_SUBSET"
|
|
|
51 |
"WF_RECURSION_THM" > "HOL4Base.relation.WF_RECURSION_THM"
|
|
|
52 |
"WF_NOT_REFL" > "HOL4Base.relation.WF_NOT_REFL"
|
|
|
53 |
"WF_INDUCTION_THM" > "HOL4Base.relation.WF_INDUCTION_THM"
|
|
|
54 |
"WF_EMPTY_REL" > "HOL4Base.relation.WF_EMPTY_REL"
|
|
|
55 |
"WF_DEF" > "HOL4Base.relation.WF_DEF"
|
|
|
56 |
"WFREC_def" > "HOL4Base.relation.WFREC_def"
|
|
|
57 |
"WFREC_THM" > "HOL4Base.relation.WFREC_THM"
|
|
|
58 |
"WFREC_DEF" > "HOL4Base.relation.WFREC_DEF"
|
|
|
59 |
"WFREC_COROLLARY" > "HOL4Base.relation.WFREC_COROLLARY"
|
|
|
60 |
"TC_def" > "HOL4Base.relation.TC_def"
|
|
|
61 |
"TC_TRANSITIVE" > "HOL4Base.relation.TC_TRANSITIVE"
|
|
|
62 |
"TC_SUBSET" > "HOL4Base.relation.TC_SUBSET"
|
|
|
63 |
"TC_STRONG_INDUCT_LEFT1" > "HOL4Base.relation.TC_STRONG_INDUCT_LEFT1"
|
|
|
64 |
"TC_STRONG_INDUCT" > "HOL4Base.relation.TC_STRONG_INDUCT"
|
|
|
65 |
"TC_RULES" > "HOL4Base.relation.TC_RULES"
|
|
|
66 |
"TC_RTC" > "HOL4Base.relation.TC_RTC"
|
|
|
67 |
"TC_RC_EQNS" > "HOL4Base.relation.TC_RC_EQNS"
|
|
|
68 |
"TC_MONOTONE" > "HOL4Base.relation.TC_MONOTONE"
|
|
|
69 |
"TC_INDUCT_LEFT1" > "HOL4Base.relation.TC_INDUCT_LEFT1"
|
|
|
70 |
"TC_INDUCT" > "HOL4Base.relation.TC_INDUCT"
|
|
|
71 |
"TC_IDEM" > "HOL4Base.relation.TC_IDEM"
|
|
|
72 |
"TC_DEF" > "HOL4Base.relation.TC_DEF"
|
|
|
73 |
"TC_CASES2" > "HOL4Base.relation.TC_CASES2"
|
|
|
74 |
"TC_CASES1" > "HOL4Base.relation.TC_CASES1"
|
|
|
75 |
"RTC_def" > "HOL4Base.relation.RTC_def"
|
|
|
76 |
"RTC_TRANSITIVE" > "HOL4Base.relation.RTC_TRANSITIVE"
|
|
|
77 |
"RTC_TC_RC" > "HOL4Base.relation.RTC_TC_RC"
|
|
|
78 |
"RTC_SUBSET" > "HOL4Base.relation.RTC_SUBSET"
|
|
|
79 |
"RTC_STRONG_INDUCT" > "HOL4Base.relation.RTC_STRONG_INDUCT"
|
|
|
80 |
"RTC_RULES" > "HOL4Base.relation.RTC_RULES"
|
|
|
81 |
"RTC_RTC" > "HOL4Base.relation.RTC_RTC"
|
|
|
82 |
"RTC_REFLEXIVE" > "HOL4Base.relation.RTC_REFLEXIVE"
|
|
|
83 |
"RTC_MONOTONE" > "HOL4Base.relation.RTC_MONOTONE"
|
|
|
84 |
"RTC_INDUCT" > "HOL4Base.relation.RTC_INDUCT"
|
|
|
85 |
"RTC_IDEM" > "HOL4Base.relation.RTC_IDEM"
|
|
|
86 |
"RTC_DEF" > "HOL4Base.relation.RTC_DEF"
|
|
|
87 |
"RTC_CASES_RTC_TWICE" > "HOL4Base.relation.RTC_CASES_RTC_TWICE"
|
|
|
88 |
"RTC_CASES2" > "HOL4Base.relation.RTC_CASES2"
|
|
|
89 |
"RTC_CASES1" > "HOL4Base.relation.RTC_CASES1"
|
|
|
90 |
"RESTRICT_def" > "HOL4Base.relation.RESTRICT_def"
|
|
|
91 |
"RESTRICT_LEMMA" > "HOL4Base.relation.RESTRICT_LEMMA"
|
|
|
92 |
"RESTRICT_DEF" > "HOL4Base.relation.RESTRICT_DEF"
|
|
|
93 |
"RC_primdef" > "HOL4Base.relation.RC_primdef"
|
|
|
94 |
"RC_def" > "HOL4Base.relation.RC_def"
|
|
|
95 |
"RC_SUBSET" > "HOL4Base.relation.RC_SUBSET"
|
|
|
96 |
"RC_RTC" > "HOL4Base.relation.RC_RTC"
|
|
|
97 |
"RC_REFLEXIVE" > "HOL4Base.relation.RC_REFLEXIVE"
|
|
|
98 |
"RC_IDEM" > "HOL4Base.relation.RC_IDEM"
|
|
|
99 |
"EMPTY_REL_def" > "HOL4Base.relation.EMPTY_REL_def"
|
|
|
100 |
"EMPTY_REL_DEF" > "HOL4Base.relation.EMPTY_REL_DEF"
|
|
|
101 |
|
|
|
102 |
end
|