From eb84cd108c7b5aef3eb41ff3bca3967ada93327b Mon Sep 17 00:00:00 2001
From: Nikita Zyuzin <nzyuzin93@gmail.com>
Date: Tue, 5 Dec 2017 01:48:10 +0100
Subject: [PATCH] Update transScript

---
 hol4/transScript.sml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/hol4/transScript.sml b/hol4/transScript.sml
index ceeb7b6..82d350a 100644
--- a/hol4/transScript.sml
+++ b/hol4/transScript.sml
@@ -1,4 +1,3 @@
-
 open preamble
 open simpLib realTheory realLib RealArith stringTheory
 
@@ -190,7 +189,7 @@ val precond_validErrorbound_true = prove (``
       \\ first_x_assum irule
       \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
       \\ rw_asm_star `absenv _ = _`
-      \\ Cases_on `absenv x12`
+      \\ Cases_on `absenv x15`
       \\ fs [])
   \\ conj_tac
   >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
@@ -240,6 +239,10 @@ val precond_validErrorbound_true = prove (``
         \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
         \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
         \\ REAL_ASM_ARITH_TAC))
+  \\ conj_tac
+  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
+      \\ rpt conj_tac \\ first_x_assum match_mp_tac
+          \\ fs [Once validIntervalbounds_def])
   \\ rpt strip_tac
   \\ rveq
   \\ fs[]
-- 
GitLab