Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/arithmetic.imp
changeset 35050 9f841f20dca6
parent 34974 18b41bba42b5
child 35092 cfe605c54e50 
--- a/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:32 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:38 2010 +0100
@@ -162,12 +162,12 @@
   "LESS_OR" > "Nat.Suc_leI"
   "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
   "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
-  "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
+  "LESS_MULT2" > "Rings.mult_pos_pos"
   "LESS_MONO_REV" > "Nat.Suc_less_SucD"
   "LESS_MONO_MULT" > "Nat.mult_le_mono1"
   "LESS_MONO_EQ" > "Nat.Suc_less_eq"
-  "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
-  "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
+  "LESS_MONO_ADD_INV" > "Groups.add_less_imp_less_right"
+  "LESS_MONO_ADD_EQ" > "Groups.add_less_cancel_right"
   "LESS_MONO_ADD" > "Nat.add_less_mono1"
   "LESS_MOD" > "Divides.mod_less"
   "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
@@ -180,7 +180,7 @@
   "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
   "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
   "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
-  "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
+  "LESS_EQ_MONO_ADD_EQ" > "Groups.add_le_cancel_right"
   "LESS_EQ_MONO" > "Nat.Suc_le_mono"
   "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
   "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
isabelle