Fix a bunch of real$abs --> realax$abs (also for min, max)

icing/CakeMLtoFloVerProofsScript.sml

@@ -278,7 +278,7 @@ Proof
     \\ rewrite_tac [REAL_LDISTRIB, REAL_MUL_RID, real_sub, REAL_NEG_ADD,
                     REAL_ADD_ASSOC]
     \\ fs[ABS_NEG, ABS_MUL]
-    \\ irule REAL_LE_TRANS \\ qexists_tac ‘1 * real$abs v’
+    \\ irule REAL_LE_TRANS \\ qexists_tac ‘1 * realax$abs v’
     \\ reverse conj_tac >- fs[]
     \\ rewrite_tac [REAL_MUL_ASSOC]
     \\ irule REAL_LE_RMUL_IMP \\ fs[ABS_POS])
@@ -1789,7 +1789,7 @@ Theorem CakeML_FloVer_infer_error:
       (empty_state, Rval [FP_WordTree fp2] ) /\
     compress_word fp = compress_word fp2 ∧
     (* the roundoff error is sound *)
-     real$abs (fp64_to_real (compress_word fp) - r) ≤ err
+     realax$abs (fp64_to_real (compress_word fp) - r) ≤ err
 Proof
   rpt strip_tac \\ fs[checkErrorbounds_succeeds_def] \\ imp_res_tac getFloVerVarMap_is_unique
   \\ qpat_x_assum `computeErrorbounds _ _ _ = SOME _` mp_tac
@@ -2040,7 +2040,7 @@ Theorem CakeML_FloVer_sound_error:
     (env with v := extend_env_with_vars (REVERSE theVars) (REVERSE vs) env.v) [body] =
       (empty_state with fp_state := empty_state.fp_state with canOpt := FPScope NoOpt, Rval [FP_WordTree fp] ) /\
     (* the roundoff error is sound *)
-     real$abs (fp64_to_real (compress_word fp) - r) ≤ err
+     realax$abs (fp64_to_real (compress_word fp) - r) ≤ err
 Proof
   rpt strip_tac
   \\ fs[isOkError_succeeds_def, isOkError_def, CaseEq "prod", CaseEq"option"]

icing/flover/CertificateCheckerScript.sml

@@ -14,7 +14,7 @@ open preambleFloVer;
 
 val _ = new_theory "CertificateChecker";
 
-Overload abs[local] = “real$abs”;
+Overload abs[local] = “realax$abs”;
 
 (** Certificate checking function **)
 Definition CertificateChecker_def:

icing/flover/EnvironmentsScript.sml

@@ -10,7 +10,7 @@ open preambleFloVer;
 
 val _ = new_theory "Environments";
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 Definition approxEnv_def:
   approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =

icing/flover/ErrorBoundsScript.sml

@@ -12,7 +12,7 @@ val _ = new_theory "ErrorBounds";
 
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 val triangle_tac =
   irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);

icing/flover/ErrorValidationScript.sml

@@ -18,7 +18,7 @@ val _ = new_theory "ErrorValidation";
 
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 val _ = realLib.prefer_real();
 

icing/flover/FPRangeValidatorScript.sml

@@ -18,7 +18,7 @@ open preambleFloVer;
 
 val _ = new_theory "FPRangeValidator";
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 Definition FPRangeValidator_def:
   FPRangeValidator (e:real expr) A typeMap dVars =

icing/flover/IEEE_connectionScript.sml

@@ -13,7 +13,7 @@ open preambleFloVer;
 
 val _ = new_theory "IEEE_connection";
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
 

icing/flover/Infra/MachineTypeScript.sml

@@ -10,7 +10,7 @@ open preambleFloVer;
 
 val _ = new_theory "MachineType";
 
-Overload abs[local] = “real$abs”
+Overload abs[local] = “realax$abs”
 
 val _ = monadsyntax.enable_monadsyntax();
 val _ = List.app monadsyntax.enable_monad ["option"];

icing/flover/Infra/RealSimpsScript.sml

@@ -7,8 +7,8 @@ open preambleFloVer;
 
 val _ = new_theory "RealSimps";
 
-Overload abs[local] = “real$abs”
-Overload max[local] = “real$max”
+Overload abs[local] = “realax$abs”
+Overload max[local] = “realax$max”
 
 Theorem abs_leq_zero[simp]:
   !v. abs v <= 0 <=> v = 0

icing/flover/IntervalArithScript.sml

@@ -10,9 +10,9 @@ val _ = temp_delsimps ["NORMEQ_CONV"]
 
 val _ = new_theory "IntervalArith";
 
-Overload abs[local] = “real$abs”
-Overload max[local] = “real$max”
-Overload min[local] = “real$min”
+Overload abs[local] = “realax$abs”
+Overload max[local] = “realax$max”
+Overload min[local] = “realax$min”
 
 (**
   Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.

icing/flover/IntervalValidationScript.sml

@@ -19,9 +19,9 @@ val _ = temp_delsimps ["RMUL_LEQNORM"]
 
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
 
-Overload abs[local] = “real$abs”
-Overload max[local] = “real$max”
-Overload min[local] = “real$min”
+Overload abs[local] = “realax$abs”
+Overload max[local] = “realax$max”
+Overload min[local] = “realax$min”
 
 (** Define a global iteration count for square roots **)
 Definition ITERCOUNT_def:

icing/flover/semantics/ExpressionSemanticsScript.sml

@@ -8,7 +8,7 @@ open preambleFloVer;
 
 val _ = new_theory "ExpressionSemantics";
 
-Overload abs = “real$abs”
+Overload abs = “realax$abs”
 
 (**
   Define a perturbation function to ease writing of basic definitions

icing/flover/semantics/ExpressionsScript.sml

@@ -7,7 +7,7 @@ open preambleFloVer;
 
 val _ = new_theory "Expressions";
 
-Overload abs = “real$abs”
+Overload abs = “realax$abs”
 
 (**
   expressions will use binary operators.