src/HOL/Import/HOL/real.imp
changeset 14847 44d92c12b255
parent 14796 1e83aa391ade
child 15647 b1f486a9c56b
     1.1 --- a/src/HOL/Import/HOL/real.imp	Sat May 29 16:47:06 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL/real.imp	Sat May 29 16:50:53 2004 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    "sumc" > "HOL4Real.real.sumc"
     1.5    "sum_def" > "HOL4Real.real.sum_def"
     1.6    "sum" > "HOL4Real.real.sum"
     1.7 -  "real_sub" > "OrderedGroup.compare_rls_1"
     1.8 +  "real_sub" > "OrderedGroup.diff_def"
     1.9    "real_of_num" > "HOL4Compat.real_of_num"
    1.10    "real_lte" > "HOL4Compat.real_lte"
    1.11    "real_lt" > "HOL.linorder_not_le"