diff --git a/metadata/entries/IEEE_Floating_Point.toml b/metadata/entries/IEEE_Floating_Point.toml
--- a/metadata/entries/IEEE_Floating_Point.toml
+++ b/metadata/entries/IEEE_Floating_Point.toml
@@ -1,53 +1,51 @@
title = "A Formal Model of IEEE Floating Point Arithmetic"
date = 2013-07-27
topics = [
"Computer science/Data structures",
]
abstract = "This development provides a formal model of IEEE-754 floating-point arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages."
license = "bsd"
note = ""
[authors]
[authors.yu]
email = "yu_email"
[contributors]
[contributors.hellauer]
email = "hellauer_email"
[contributors.immler]
homepage = "immler_homepage"
[contributors.weber]
email = "weber_email"
[notify]
paulson = "paulson_email"
immler = "immler_email"
weber = "weber_email"
[history]
2017-09-25 = """
Added conversions from and to software floating point numbers
(by Fabian Hellauer and Fabian Immler).
"""
2018-02-05 = """
'Modernized' representation following the formalization in HOL4:
former \"float_format\" and predicate \"is_valid\" is now encoded in a type \"('e, 'f) float\" where
'e and 'f encode the size of exponent and fraction.
"""
2023-05-10 = """
Added the IEEE rounding mode \"roundNearestTiesToAway\".
"""
2023-05-22 = """
Added a model of floating-point arithmetic with a single NaN value.
-"""
-2023-05-22 = """
Added a translation of floating-point arithmetic into SMT-LIB.
"""
[extra]
[related]