--- a/src/HOL/Import/HOL/arithmetic.imp Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp Thu May 17 19:49:40 2007 +0200
@@ -14,19 +14,19 @@
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
- "MOD" > "Divides.mod" :: "nat => nat => nat"
"MIN" > "Orderings.min" :: "nat => nat => nat"
"MAX" > "Orderings.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
- "EXP" > "Nat.power" :: "nat => nat => nat"
- "DIV" > "Divides.div" :: "nat => nat => nat"
+ "EXP" > "Nat.power_class.power" :: "nat => nat => nat"
+ "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
+ "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
- "<=" > "Orderings.less_eq" :: "nat => nat => bool"
- "-" > "HOL.minus" :: "nat => nat => nat"
- "+" > "HOL.plus" :: "nat => nat => nat"
- "*" > "HOL.times" :: "nat => nat => nat"
+ "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
+ "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+ "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
+ "*" > "HOL.times_class.times" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"