# HG changeset patch
# User blanchet
# Date 1323854308 -3600
# Node ID 36ff12b5663bf4de03d622c3c3a211a1c5d53699
# Parent  9ae1c60db357238d55b0fd4674635181238d6021
fixed Nitpick definition of "<" on "real"s

diff -r 9ae1c60db357 -r 36ff12b5663b src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Dec 14 08:32:48 2011 +0100
+++ b/src/HOL/RealDef.thy	Wed Dec 14 10:18:28 2011 +0100
@@ -1767,7 +1767,7 @@
     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
-    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}),
+    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
 *}