# HG changeset patch # User haftmann # Date 1265788480 -3600 # Node ID 22bdb7f86a1eda34fd3780769dcd661a3dd66a2e # Parent e25eedfc15ce053ea499e97064e7fdc7aac6da21 moved constants inverse and divide to Ring.thy diff -r e25eedfc15ce -r 22bdb7f86a1e src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Wed Feb 10 08:54:40 2010 +0100 @@ -17,7 +17,7 @@ "real_ge" > "HOL4Compat.real_ge" "pow" > "Power.power_class.power" :: "real => nat => real" "abs" > "Algebras.abs" :: "real => real" - "/" > "Algebras.divide" :: "real => real => real" + "/" > "Ring.divide" :: "real => real => real" thm_maps "sup_def" > "HOL4Real.real.sup_def" @@ -31,7 +31,7 @@ "real_lt" > "Orderings.linorder_not_le" "real_gt" > "HOL4Compat.real_gt" "real_ge" > "HOL4Compat.real_ge" - "real_div" > "Rings.field_class.divide_inverse" + "real_div" > "Ring.divide_inverse" "pow" > "HOL4Compat.pow" "abs" > "HOL4Compat.abs" "SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"