Skip to content
Snippets Groups Projects
Commit 80f7f122 authored by Heiko Becker's avatar Heiko Becker
Browse files

Use OLD_REAL_ASM_ARITH_TAC in FpRangeValidator

parent dfdd8e02
No related branches found
No related tags found
No related merge requests found
...@@ -130,8 +130,8 @@ val solve_tac = ...@@ -130,8 +130,8 @@ val solve_tac =
\\ every_case_tac \\ fs[] \\ every_case_tac \\ fs[]
\\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/ \\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/
abs v <= abs (SND (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) by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.OLD_REAL_ASM_ARITH_TAC)
\\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC); \\ TRY (every_case_tac \\ RealArith.OLD_REAL_ASM_ARITH_TAC);
Theorem FPRangeValidator_sound: Theorem FPRangeValidator_sound:
e E1 E2 Gamma v m A fVars (dVars:num_set). e E1 E2 Gamma v m A fVars (dVars:num_set).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment