more operations;

--- a/src/Pure/library.ML	Tue Sep 17 17:51:55 2024 +0200
+++ b/src/Pure/library.ML	Tue Sep 17 18:49:46 2024 +0200
@@ -165,6 +165,7 @@
   val match_string: string -> string -> bool
 
   (*reals*)
+  val eq_real: real * real -> bool
   val string_of_real: real -> string
   val signed_string_of_real: real -> string
 
@@ -813,6 +814,8 @@
 
 (** reals **)
 
+fun eq_real (a, b) = Real.isNan a andalso Real.isNan b orelse Real.== (a, b);
+
 val string_of_real = Real.fmt (StringCvt.GEN NONE);
 
 fun signed_string_of_real x =