179 NUMERAL > HOL4Compat.NUMERAL |
179 NUMERAL > HOL4Compat.NUMERAL |
180 num_case > Nat.nat.nat_case |
180 num_case > Nat.nat.nat_case |
181 ">" > HOL4Compat.nat_gt |
181 ">" > HOL4Compat.nat_gt |
182 ">=" > HOL4Compat.nat_ge |
182 ">=" > HOL4Compat.nat_ge |
183 FUNPOW > HOL4Compat.FUNPOW |
183 FUNPOW > HOL4Compat.FUNPOW |
184 "<=" > HOL.ord_class.less_eq :: "[nat,nat]=>bool" |
184 "<=" > Algebras.less_eq :: "[nat,nat]=>bool" |
185 "+" > HOL.plus_class.plus :: "[nat,nat]=>nat" |
185 "+" > Algebras.plus :: "[nat,nat]=>nat" |
186 "*" > HOL.times_class.times :: "[nat,nat]=>nat" |
186 "*" > Algebras.times :: "[nat,nat]=>nat" |
187 "-" > HOL.minus_class.minus :: "[nat,nat]=>nat" |
187 "-" > Algebras.minus :: "[nat,nat]=>nat" |
188 MIN > Orderings.ord_class.min :: "[nat,nat]=>nat" |
188 MIN > Orderings.min :: "[nat,nat]=>nat" |
189 MAX > Orderings.ord_class.max :: "[nat,nat]=>nat" |
189 MAX > Orderings.max :: "[nat,nat]=>nat" |
190 DIV > Divides.div_class.div :: "[nat,nat]=>nat" |
190 DIV > Divides.div :: "[nat,nat]=>nat" |
191 MOD > Divides.div_class.mod :: "[nat,nat]=>nat" |
191 MOD > Divides.mod :: "[nat,nat]=>nat" |
192 EXP > Power.power_class.power :: "[nat,nat]=>nat"; |
192 EXP > Power.power :: "[nat,nat]=>nat"; |
193 |
193 |
194 end_import; |
194 end_import; |
195 |
195 |
196 import_theory hrat; |
196 import_theory hrat; |
197 end_import; |
197 end_import; |