diff --git a/icing/flover/IEEE_connectionScript.sml b/icing/flover/IEEE_connectionScript.sml index c1e4081274..899bb49b2a 100644 --- a/icing/flover/IEEE_connectionScript.sml +++ b/icing/flover/IEEE_connectionScript.sml @@ -15,8 +15,6 @@ val _ = new_theory "IEEE_connection"; Overload abs[local] = “realax$abs” -val _ = diminish_srw_ss ["RMULCANON","RMULRELNORM"] - (** FloVer assumes rounding with ties to even, thus we exprlicitly define a rounding mode here **) Definition dmode_def :