| author | boehmes |
| Tue, 27 Mar 2012 17:11:02 +0200 | |
| changeset 47155 | ade3fc826af3 |
| parent 46787 | 3d3d8f8929a7 |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"nat_elim__magic" > "nat_elim__magic_def" |
|
7 |
"ODD" > "ODD_def" |
|
8 |
"FACT" > "FACT_def" |
|
9 |
"EVEN" > "EVEN_def" |
|
10 |
||
11 |
const_maps |
|
12 |
"num_case" > "Nat.nat.nat_case" |
|
13 |
"nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
14 |
"NUMERAL_BIT2" > "Compatibility.NUMERAL_BIT2" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
15 |
"NUMERAL_BIT1" > "Compatibility.NUMERAL_BIT1" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
16 |
"NUMERAL" > "Compatibility.NUMERAL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
17 |
"MOD" > "Divides.div_class.mod" :: "nat => nat => nat" |
| 23132 | 18 |
"MIN" > "Orderings.ord_class.min" :: "nat => nat => nat" |
19 |
"MAX" > "Orderings.ord_class.max" :: "nat => nat => nat" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
20 |
"FUNPOW" > "Compatibility.FUNPOW" |
| 24996 | 21 |
"EXP" > "Power.power_class.power" :: "nat => nat => nat" |
| 22997 | 22 |
"DIV" > "Divides.div_class.div" :: "nat => nat => nat" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
23 |
"ALT_ZERO" > "Compatibility.ALT_ZERO" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
24 |
">=" > "Compatibility.nat_ge" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
25 |
">" > "Compatibility.nat_gt" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
26 |
"<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
27 |
"-" > "Groups.minus_class.minus" :: "nat => nat => nat" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
28 |
"+" > "Groups.plus_class.plus" :: "nat => nat => nat" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
29 |
"*" > "Groups.times_class.times" :: "nat => nat => nat" |
| 14516 | 30 |
|
31 |
thm_maps |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
32 |
"num_case_def" > "Compatibility.num_case_def" |
| 14516 | 33 |
"num_case_cong" > "HOL4Base.arithmetic.num_case_cong" |
34 |
"num_case_compute" > "HOL4Base.arithmetic.num_case_compute" |
|
35 |
"num_CASES" > "Nat.nat.nchotomy" |
|
36 |
"nat_elim__magic_def" > "HOL4Base.arithmetic.nat_elim__magic_def" |
|
37 |
"nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic" |
|
38 |
"ZERO_MOD" > "HOL4Base.arithmetic.ZERO_MOD" |
|
39 |
"ZERO_LESS_EXP" > "HOL4Base.arithmetic.ZERO_LESS_EXP" |
|
40 |
"ZERO_LESS_EQ" > "Nat.le0" |
|
41 |
"ZERO_DIV" > "HOL4Base.arithmetic.ZERO_DIV" |
|
42 |
"WOP" > "HOL4Base.arithmetic.WOP" |
|
43 |
"TWO" > "HOL4Base.arithmetic.TWO" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
44 |
"TIMES2" > "Int.semiring_mult_2" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
45 |
"SUC_SUB1" > "Nat.diff_Suc_1" |
| 31790 | 46 |
"SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
47 |
"SUC_NOT" > "Nat.Zero_not_Suc" |
| 14516 | 48 |
"SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM" |
49 |
"SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM" |
|
| 21243 | 50 |
"SUB_SUB" > "Nat.diff_diff_right" |
| 14516 | 51 |
"SUB_RIGHT_SUB" > "Nat.diff_diff_left" |
52 |
"SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ" |
|
53 |
"SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS" |
|
54 |
"SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ" |
|
55 |
"SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER" |
|
56 |
"SUB_RIGHT_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_EQ" |
|
57 |
"SUB_RIGHT_ADD" > "HOL4Base.arithmetic.SUB_RIGHT_ADD" |
|
58 |
"SUB_PLUS" > "Nat.diff_diff_left" |
|
59 |
"SUB_MONO_EQ" > "Nat.diff_Suc_Suc" |
|
60 |
"SUB_LESS_OR" > "HOL4Base.arithmetic.SUB_LESS_OR" |
|
61 |
"SUB_LESS_EQ_ADD" > "HOL4Base.arithmetic.SUB_LESS_EQ_ADD" |
|
62 |
"SUB_LESS_EQ" > "Nat.diff_le_self" |
|
63 |
"SUB_LESS_0" > "Nat.zero_less_diff" |
|
64 |
"SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC" |
|
65 |
"SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB" |
|
66 |
"SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ" |
|
| 21243 | 67 |
"SUB_LEFT_LESS" > "Nat.less_diff_conv" |
68 |
"SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv" |
|
| 14516 | 69 |
"SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER" |
70 |
"SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ" |
|
71 |
"SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD" |
|
72 |
"SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0" |
|
73 |
"SUB_EQ_0" > "Nat.diff_is_0_eq" |
|
74 |
"SUB_EQUAL_0" > "Nat.diff_self_eq_0" |
|
75 |
"SUB_ELIM_THM" > "HOL4Base.arithmetic.SUB_ELIM_THM" |
|
76 |
"SUB_CANCEL" > "HOL4Base.arithmetic.SUB_CANCEL" |
|
77 |
"SUB_ADD" > "Nat.le_add_diff_inverse2" |
|
78 |
"SUB_0" > "HOL4Base.arithmetic.SUB_0" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
79 |
"SUB" > "Compatibility.SUB" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
80 |
"RIGHT_SUB_DISTRIB" > "Nat.diff_mult_distrib" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
81 |
"RIGHT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_26" |
| 14516 | 82 |
"PRE_SUC_EQ" > "HOL4Base.arithmetic.PRE_SUC_EQ" |
83 |
"PRE_SUB1" > "HOL4Base.arithmetic.PRE_SUB1" |
|
84 |
"PRE_SUB" > "HOL4Base.arithmetic.PRE_SUB" |
|
85 |
"PRE_ELIM_THM" > "HOL4Base.arithmetic.PRE_ELIM_THM" |
|
86 |
"OR_LESS" > "Nat.Suc_le_lessD" |
|
87 |
"ONE" > "Nat.One_nat_def" |
|
88 |
"ODD_OR_EVEN" > "HOL4Base.arithmetic.ODD_OR_EVEN" |
|
89 |
"ODD_MULT" > "HOL4Base.arithmetic.ODD_MULT" |
|
90 |
"ODD_EXISTS" > "HOL4Base.arithmetic.ODD_EXISTS" |
|
91 |
"ODD_EVEN" > "HOL4Base.arithmetic.ODD_EVEN" |
|
92 |
"ODD_DOUBLE" > "HOL4Base.arithmetic.ODD_DOUBLE" |
|
93 |
"ODD_ADD" > "HOL4Base.arithmetic.ODD_ADD" |
|
94 |
"ODD" > "HOL4Base.arithmetic.ODD" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
95 |
"NUMERAL_DEF" > "Compatibility.NUMERAL_def" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
96 |
"NUMERAL_BIT2" > "Compatibility.NUMERAL_BIT2_def" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
97 |
"NUMERAL_BIT1" > "Compatibility.NUMERAL_BIT1_def" |
| 14516 | 98 |
"NOT_ZERO_LT_ZERO" > "Nat.neq0_conv" |
99 |
"NOT_SUC_LESS_EQ_0" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ_0" |
|
100 |
"NOT_SUC_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ" |
|
101 |
"NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ" |
|
102 |
"NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN" |
|
103 |
"NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
104 |
"NOT_LESS_EQUAL" > "Orderings.linorder_class.not_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
105 |
"NOT_LESS" > "Orderings.linorder_class.not_less" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
106 |
"NOT_LEQ" > "Nat.not_less_eq_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
107 |
"NOT_GREATER_EQ" > "Nat.not_less_eq_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
108 |
"NOT_GREATER" > "Orderings.linorder_class.not_less" |
| 14516 | 109 |
"NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0" |
110 |
"NORM_0" > "HOL4Base.arithmetic.NORM_0" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
111 |
"MULT_SYM" > "Fields.linordered_field_class.sign_simps_40" |
| 14516 | 112 |
"MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ" |
113 |
"MULT_SUC" > "Nat.mult_Suc_right" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
114 |
"MULT_RIGHT_1" > "Divides.arithmetic_simps_43" |
| 14516 | 115 |
"MULT_MONO_EQ" > "Nat.Suc_mult_cancel1" |
116 |
"MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
117 |
"MULT_LEFT_1" > "Divides.arithmetic_simps_42" |
| 14516 | 118 |
"MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES" |
119 |
"MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
120 |
"MULT_EQ_1" > "Nat.nat_mult_eq_1_iff" |
| 14516 | 121 |
"MULT_EQ_0" > "Nat.mult_is_0" |
122 |
"MULT_DIV" > "Divides.div_mult_self_is_m" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
123 |
"MULT_COMM" > "Fields.linordered_field_class.sign_simps_40" |
| 14516 | 124 |
"MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
125 |
"MULT_ASSOC" > "Fields.linordered_field_class.sign_simps_41" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
126 |
"MULT_0" > "Divides.arithmetic_simps_41" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
127 |
"MULT" > "Compatibility.MULT" |
| 14516 | 128 |
"MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE" |
129 |
"MOD_TIMES2" > "HOL4Base.arithmetic.MOD_TIMES2" |
|
130 |
"MOD_TIMES" > "HOL4Base.arithmetic.MOD_TIMES" |
|
131 |
"MOD_PLUS" > "HOL4Base.arithmetic.MOD_PLUS" |
|
132 |
"MOD_P" > "HOL4Base.arithmetic.MOD_P" |
|
133 |
"MOD_ONE" > "Divides.mod_1" |
|
134 |
"MOD_MULT_MOD" > "HOL4Base.arithmetic.MOD_MULT_MOD" |
|
135 |
"MOD_MULT" > "HOL4Base.arithmetic.MOD_MULT" |
|
136 |
"MOD_MOD" > "HOL4Base.arithmetic.MOD_MOD" |
|
137 |
"MOD_EQ_0" > "HOL4Base.arithmetic.MOD_EQ_0" |
|
138 |
"MOD_COMMON_FACTOR" > "HOL4Base.arithmetic.MOD_COMMON_FACTOR" |
|
139 |
"MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED" |
|
140 |
"MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT" |
|
141 |
"MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ" |
|
142 |
"MIN_LT" > "HOL4Base.arithmetic.MIN_LT" |
|
143 |
"MIN_LE" > "HOL4Base.arithmetic.MIN_LE" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
144 |
"MIN_IDEM" > "Big_Operators.linorder_class.Min.idem" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
145 |
"MIN_DEF" > "Compatibility.MIN_DEF" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
146 |
"MIN_COMM" > "Lattices.linorder_class.min_max.inf.commute" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
147 |
"MIN_ASSOC" > "Lattices.linorder_class.min_max.inf.assoc" |
| 14516 | 148 |
"MIN_0" > "HOL4Base.arithmetic.MIN_0" |
149 |
"MAX_LT" > "HOL4Base.arithmetic.MAX_LT" |
|
150 |
"MAX_LE" > "HOL4Base.arithmetic.MAX_LE" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
151 |
"MAX_IDEM" > "Big_Operators.linorder_class.Max.idem" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
152 |
"MAX_DEF" > "Compatibility.MAX_DEF" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
153 |
"MAX_COMM" > "Lattices.linorder_class.min_max.inf_sup_aci_5" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
154 |
"MAX_ASSOC" > "Lattices.linorder_class.min_max.inf_sup_aci_6" |
| 14516 | 155 |
"MAX_0" > "HOL4Base.arithmetic.MAX_0" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
156 |
"LESS_TRANS" > "Orderings.order_less_trans" |
| 14516 | 157 |
"LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT" |
158 |
"LESS_SUC_EQ_COR" > "Nat.Suc_lessI" |
|
159 |
"LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS" |
|
160 |
"LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
161 |
"LESS_OR_EQ" > "Compatibility.LESS_OR_EQ" |
| 14516 | 162 |
"LESS_OR" > "Nat.Suc_leI" |
163 |
"LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC" |
|
164 |
"LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
165 |
"LESS_MULT2" > "Rings.linordered_semiring_strict_class.mult_pos_pos" |
| 14516 | 166 |
"LESS_MONO_REV" > "Nat.Suc_less_SucD" |
167 |
"LESS_MONO_MULT" > "Nat.mult_le_mono1" |
|
168 |
"LESS_MONO_EQ" > "Nat.Suc_less_eq" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
169 |
"LESS_MONO_ADD_INV" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_imp_less_right" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
170 |
"LESS_MONO_ADD_EQ" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
171 |
"LESS_MONO_ADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_right_mono" |
| 14516 | 172 |
"LESS_MOD" > "Divides.mod_less" |
173 |
"LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
174 |
"LESS_LESS_EQ_TRANS" > "Orderings.order_less_le_trans" |
| 14516 | 175 |
"LESS_LESS_CASES" > "HOL4Base.arithmetic.LESS_LESS_CASES" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
176 |
"LESS_IMP_LESS_OR_EQ" > "FunDef.termination_basic_simps_5" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
177 |
"LESS_IMP_LESS_ADD" > "FunDef.termination_basic_simps_1" |
| 14516 | 178 |
"LESS_EXP_SUC_MONO" > "HOL4Base.arithmetic.LESS_EXP_SUC_MONO" |
179 |
"LESS_EQ_TRANS" > "Nat.le_trans" |
|
180 |
"LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL" |
|
181 |
"LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
182 |
"LESS_EQ_REFL" > "Nat.le_refl" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
183 |
"LESS_EQ_MONO_ADD_EQ" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right" |
| 14516 | 184 |
"LESS_EQ_MONO" > "Nat.Suc_le_mono" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
185 |
"LESS_EQ_LESS_TRANS" > "Orderings.order_le_less_trans" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
186 |
"LESS_EQ_LESS_EQ_MONO" > "Groups.add_mono_thms_linordered_semiring_1" |
| 14516 | 187 |
"LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc" |
| 21243 | 188 |
"LESS_EQ_EXISTS" > "Nat.le_iff_add" |
| 14516 | 189 |
"LESS_EQ_CASES" > "Nat.nat_le_linear" |
190 |
"LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM" |
|
| 21243 | 191 |
"LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc" |
| 14516 | 192 |
"LESS_EQ_ADD" > "Nat.le_add1" |
193 |
"LESS_EQ_0" > "Nat.le_0_eq" |
|
| 33657 | 194 |
"LESS_EQUAL_ANTISYM" > "Nat.le_antisym" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
195 |
"LESS_EQUAL_ADD" > "Series.le_Suc_ex" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
196 |
"LESS_EQ" > "Nat.Suc_le_eq" |
| 14516 | 197 |
"LESS_DIV_EQ_ZERO" > "Divides.div_less" |
198 |
"LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP" |
|
199 |
"LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES" |
|
200 |
"LESS_ANTISYM" > "HOL4Base.arithmetic.LESS_ANTISYM" |
|
201 |
"LESS_ADD_SUC" > "HOL4Base.arithmetic.LESS_ADD_SUC" |
|
202 |
"LESS_ADD_NONZERO" > "HOL4Base.arithmetic.LESS_ADD_NONZERO" |
|
203 |
"LESS_ADD_1" > "HOL4Base.arithmetic.LESS_ADD_1" |
|
204 |
"LESS_ADD" > "HOL4Base.arithmetic.LESS_ADD" |
|
205 |
"LESS_0_CASES" > "HOL4Base.arithmetic.LESS_0_CASES" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
206 |
"LEFT_SUB_DISTRIB" > "Nat.diff_mult_distrib2" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
207 |
"LEFT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_25" |
| 14516 | 208 |
"LE" > "HOL4Base.arithmetic.LE" |
209 |
"INV_PRE_LESS_EQ" > "HOL4Base.arithmetic.INV_PRE_LESS_EQ" |
|
210 |
"INV_PRE_LESS" > "HOL4Base.arithmetic.INV_PRE_LESS" |
|
211 |
"INV_PRE_EQ" > "HOL4Base.arithmetic.INV_PRE_EQ" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
212 |
"GREATER_OR_EQ" > "Compatibility.GREATER_OR_EQ" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
213 |
"GREATER_EQ" > "Compatibility.real_ge" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
214 |
"GREATER_DEF" > "Compatibility.GREATER_DEF" |
| 14516 | 215 |
"FUN_EQ_LEMMA" > "HOL4Base.arithmetic.FUN_EQ_LEMMA" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
216 |
"FUNPOW" > "Compatibility.FUNPOW" |
| 14516 | 217 |
"FACT_LESS" > "HOL4Base.arithmetic.FACT_LESS" |
218 |
"FACT" > "HOL4Base.arithmetic.FACT" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
219 |
"EXP_INJECTIVE" > "Power.linordered_semidom_class.power_inject_exp" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
220 |
"EXP_EQ_1" > "Primes.exp_eq_1" |
| 14516 | 221 |
"EXP_EQ_0" > "HOL4Base.arithmetic.EXP_EQ_0" |
222 |
"EXP_ALWAYS_BIG_ENOUGH" > "HOL4Base.arithmetic.EXP_ALWAYS_BIG_ENOUGH" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
223 |
"EXP_ADD" > "Power.monoid_mult_class.power_add" |
| 14516 | 224 |
"EXP_1" > "HOL4Base.arithmetic.EXP_1" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
225 |
"EXP" > "Compatibility.EXP" |
| 14516 | 226 |
"EXISTS_GREATEST" > "HOL4Base.arithmetic.EXISTS_GREATEST" |
227 |
"EVEN_OR_ODD" > "HOL4Base.arithmetic.EVEN_OR_ODD" |
|
228 |
"EVEN_ODD_EXISTS" > "HOL4Base.arithmetic.EVEN_ODD_EXISTS" |
|
229 |
"EVEN_ODD" > "HOL4Base.arithmetic.EVEN_ODD" |
|
230 |
"EVEN_MULT" > "HOL4Base.arithmetic.EVEN_MULT" |
|
231 |
"EVEN_EXISTS" > "HOL4Base.arithmetic.EVEN_EXISTS" |
|
232 |
"EVEN_DOUBLE" > "HOL4Base.arithmetic.EVEN_DOUBLE" |
|
233 |
"EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD" |
|
234 |
"EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD" |
|
235 |
"EVEN" > "HOL4Base.arithmetic.EVEN" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
236 |
"EQ_MULT_LCANCEL" > "Numeral_Simprocs.nat_mult_eq_cancel_disj" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
237 |
"EQ_MONO_ADD_EQ" > "Groups.cancel_semigroup_add_class.add_right_cancel" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
238 |
"EQ_LESS_EQ" > "Orderings.order_class.eq_iff" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
239 |
"EQ_ADD_RCANCEL" > "Groups.cancel_semigroup_add_class.add_right_cancel" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
240 |
"EQ_ADD_LCANCEL" > "Groups.cancel_semigroup_add_class.add_left_cancel" |
| 14516 | 241 |
"DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE" |
242 |
"DIV_P" > "HOL4Base.arithmetic.DIV_P" |
|
243 |
"DIV_ONE" > "Divides.div_1" |
|
244 |
"DIV_MULT" > "HOL4Base.arithmetic.DIV_MULT" |
|
245 |
"DIV_LESS_EQ" > "HOL4Base.arithmetic.DIV_LESS_EQ" |
|
246 |
"DIV_LESS" > "Divides.div_less_dividend" |
|
247 |
"DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT" |
|
248 |
"DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
249 |
"DIVISION" > "Compatibility.DIVISION" |
| 14516 | 250 |
"DA" > "HOL4Base.arithmetic.DA" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
251 |
"COMPLETE_INDUCTION" > "Nat.nat_less_induct" |
| 21243 | 252 |
"CANCEL_SUB" > "Nat.eq_diff_iff" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
253 |
"ALT_ZERO" > "Compatibility.ALT_ZERO_def" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
254 |
"ADD_SYM" > "Fields.linordered_field_class.sign_simps_43" |
| 14516 | 255 |
"ADD_SUC" > "Nat.add_Suc_right" |
256 |
"ADD_SUB" > "Nat.diff_add_inverse2" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
257 |
"ADD_MONO_LESS_EQ" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left" |
| 14516 | 258 |
"ADD_INV_0_EQ" > "HOL4Base.arithmetic.ADD_INV_0_EQ" |
259 |
"ADD_INV_0" > "Nat.add_eq_self_zero" |
|
260 |
"ADD_EQ_SUB" > "HOL4Base.arithmetic.ADD_EQ_SUB" |
|
261 |
"ADD_EQ_1" > "HOL4Base.arithmetic.ADD_EQ_1" |
|
262 |
"ADD_EQ_0" > "Nat.add_is_0" |
|
263 |
"ADD_DIV_ADD_DIV" > "HOL4Base.arithmetic.ADD_DIV_ADD_DIV" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
264 |
"ADD_COMM" > "Fields.linordered_field_class.sign_simps_43" |
| 14516 | 265 |
"ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
266 |
"ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_44" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35267
diff
changeset
|
267 |
"ADD_0" > "Divides.arithmetic_simps_39" |
| 31790 | 268 |
"ADD1" > "Nat_Numeral.Suc_eq_plus1" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
44763
diff
changeset
|
269 |
"ADD" > "Compatibility.ADD" |
| 14516 | 270 |
|
271 |
end |