--- a/src/HOL/Import/HOL/arithmetic.imp Fri Feb 19 14:47:00 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Feb 19 14:47:01 2010 +0100
@@ -24,9 +24,9 @@
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
"<=" > "Orderings.less_eq" :: "nat => nat => bool"
- "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
- "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
- "*" > "Algebras.times_class.times" :: "nat => nat => nat"
+ "-" > "Groups.minus" :: "nat => nat => nat"
+ "+" > "Groups.plus" :: "nat => nat => nat"
+ "*" > "Groups.times" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"