# HG changeset patch
# User wenzelm
# Date 1726591786 -7200
# Node ID 71756d95b7df9da74716f0c51ebbdeca42aabfda
# Parent  5328d67ec64761388b6f7ad73a1fd350b841c15f
more operations;

diff -r 5328d67ec647 -r 71756d95b7df src/Pure/library.ML
--- 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 =