src/HOL/Import/HOL/arithmetic.imp
changeset 35050 9f841f20dca6
parent 34974 18b41bba42b5
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -162,12 +162,12 @@
     1.4    "LESS_OR" > "Nat.Suc_leI"
     1.5    "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
     1.6    "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
     1.7 -  "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
     1.8 +  "LESS_MULT2" > "Rings.mult_pos_pos"
     1.9    "LESS_MONO_REV" > "Nat.Suc_less_SucD"
    1.10    "LESS_MONO_MULT" > "Nat.mult_le_mono1"
    1.11    "LESS_MONO_EQ" > "Nat.Suc_less_eq"
    1.12 -  "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
    1.13 -  "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
    1.14 +  "LESS_MONO_ADD_INV" > "Groups.add_less_imp_less_right"
    1.15 +  "LESS_MONO_ADD_EQ" > "Groups.add_less_cancel_right"
    1.16    "LESS_MONO_ADD" > "Nat.add_less_mono1"
    1.17    "LESS_MOD" > "Divides.mod_less"
    1.18    "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
    1.19 @@ -180,7 +180,7 @@
    1.20    "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
    1.21    "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
    1.22    "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
    1.23 -  "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
    1.24 +  "LESS_EQ_MONO_ADD_EQ" > "Groups.add_le_cancel_right"
    1.25    "LESS_EQ_MONO" > "Nat.Suc_le_mono"
    1.26    "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
    1.27    "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"