From 80f7f122f952397ba9ed05a81d1e573422ac777b Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Wed, 13 Jul 2022 16:41:51 +0200
Subject: [PATCH] Use OLD_REAL_ASM_ARITH_TAC in FpRangeValidator
---
hol4/FPRangeValidatorScript.sml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index bd81e50..5e315ca 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -130,8 +130,8 @@ val solve_tac =
\\ every_case_tac \\ fs[]
\\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/
abs v <= abs (SND (widenInterval iv_e err_e))`
- by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
- \\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
+ by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.OLD_REAL_ASM_ARITH_TAC)
+ \\ TRY (every_case_tac \\ RealArith.OLD_REAL_ASM_ARITH_TAC);
Theorem FPRangeValidator_sound:
∀ e E1 E2 Gamma v m A fVars (dVars:num_set).
--
GitLab