src/HOL/Import/HOL/real.imp

   "real_of_num" > "HOL4Compat.real_of_num"
   "real_lte" > "HOL4Compat.real_lte"
   "real_lt" > "Orderings.linorder_not_le"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
-  "real_div" > "Ring_and_Field.field.divide_inverse"
+  "real_div" > "Ring_and_Field.field_class.divide_inverse"
   "pow" > "HOL4Compat.pow"
   "abs" > "HOL4Compat.abs"
   "SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3"
   "SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2"
   "SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1"

   "REAL_MEAN" > "Ring_and_Field.dense"
   "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
   "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
   "REAL_LT_SUB_RADD" > "OrderedGroup.compare_rls_6"
   "REAL_LT_SUB_LADD" > "OrderedGroup.compare_rls_7"
-  "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict.mult_strict_right_mono"
+  "REAL_LT_RMUL_IMP" > "Ring_and_Field.ordered_semiring_strict_class.mult_strict_right_mono"
   "REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0"
   "REAL_LT_RMUL" > "RealDef.real_mult_less_iff1"
   "REAL_LT_REFL" > "Orderings.order_less_irrefl"
   "REAL_LT_RDIV_EQ" > "Ring_and_Field.pos_less_divide_eq"
   "REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0"

   "REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL"
   "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less"
   "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
   "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'"
   "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
-  "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono"
+  "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict_class.mult_strict_mono"
   "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
   "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
-  "REAL_LT_LE" > "Orderings.order.order_less_le"
+  "REAL_LT_LE" > "Orderings.order_class.order_less_le"
   "REAL_LT_LDIV_EQ" > "Ring_and_Field.pos_divide_less_eq"
   "REAL_LT_LADD" > "OrderedGroup.add_less_cancel_left"
   "REAL_LT_INV_EQ" > "Ring_and_Field.inverse_positive_iff_positive"
   "REAL_LT_INV" > "Ring_and_Field.less_imp_inverse_less"
   "REAL_LT_IMP_NE" > "Orderings.less_imp_neq"

   "REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL"
   "REAL_LT_ADD2" > "OrderedGroup.add_strict_mono"
   "REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1"
   "REAL_LT_ADD" > "OrderedGroup.add_pos_pos"
   "REAL_LT_1" > "HOL4Real.real.REAL_LT_1"
-  "REAL_LT_01" > "Ring_and_Field.ordered_semidom.zero_less_one"
+  "REAL_LT_01" > "Ring_and_Field.ordered_semidom_class.zero_less_one"
   "REAL_LTE_TRANS" > "Set.basic_trans_rules_24"
   "REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL"
   "REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM"
   "REAL_LTE_ADD2" > "OrderedGroup.add_less_le_mono"
   "REAL_LTE_ADD" > "OrderedGroup.add_pos_nonneg"
   "REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2"
   "REAL_LT" > "RealDef.real_of_nat_less_iff"
   "REAL_LNEG_UNIQ" > "HOL4Real.real.REAL_LNEG_UNIQ"
   "REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ"
   "REAL_LE_TRANS" > "Set.basic_trans_rules_25"
-  "REAL_LE_TOTAL" > "Orderings.linorder.linorder_linear"
+  "REAL_LE_TOTAL" > "Orderings.linorder_class.linorder_linear"
   "REAL_LE_SUB_RADD" > "OrderedGroup.compare_rls_8"
   "REAL_LE_SUB_LADD" > "OrderedGroup.compare_rls_9"
   "REAL_LE_SQUARE" > "Ring_and_Field.zero_le_square"
   "REAL_LE_RNEG" > "OrderedGroup.le_eq_neg"
-  "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring.mult_right_mono"
+  "REAL_LE_RMUL_IMP" > "Ring_and_Field.pordered_semiring_class.mult_right_mono"
   "REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1"
   "REAL_LE_REFL" > "Finite_Set.max.f_below.below_refl"
   "REAL_LE_RDIV_EQ" > "Ring_and_Field.pos_le_divide_eq"
   "REAL_LE_RDIV" > "Ring_and_Field.mult_imp_le_div_pos"
   "REAL_LE_RADD" > "OrderedGroup.add_le_cancel_right"

   "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le"
   "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
   "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg"
   "REAL_LE_LT" > "Orderings.order_le_less"
   "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
-  "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
+  "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring_class.mult_mono"
   "REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2"
   "REAL_LE_LDIV_EQ" > "Ring_and_Field.pos_divide_le_eq"
   "REAL_LE_LDIV" > "Ring_and_Field.mult_imp_div_pos_le"
-  "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add.add_left_mono"
+  "REAL_LE_LADD_IMP" > "OrderedGroup.pordered_ab_semigroup_add_class.add_left_mono"
   "REAL_LE_LADD" > "OrderedGroup.add_le_cancel_left"
   "REAL_LE_INV_EQ" > "Ring_and_Field.inverse_nonnegative_iff_nonnegative"
   "REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV"
   "REAL_LE_DOUBLE" > "OrderedGroup.zero_le_double_add_iff_zero_le_single_add"
   "REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV"

   "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
   "REAL_INV_LT1" > "RealDef.real_inverse_gt_one"
   "REAL_INV_INV" > "Ring_and_Field.inverse_inverse_eq"
   "REAL_INV_EQ_0" > "Ring_and_Field.inverse_nonzero_iff_nonzero"
   "REAL_INV_1OVER" > "Ring_and_Field.inverse_eq_divide"
-  "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
+  "REAL_INV_0" > "Ring_and_Field.division_by_zero_class.inverse_zero"
   "REAL_INVINV" > "Ring_and_Field.nonzero_inverse_inverse_eq"
   "REAL_INV1" > "Ring_and_Field.inverse_1"
   "REAL_INJ" > "RealDef.real_of_nat_inject"
   "REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
   "REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"