diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 7bd665a803240ec0122456a22b1119b2e49b7031..49dc781630440f36a47cc1af21743693b9b4aad1 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -2323,9 +2323,9 @@ Proof
   \\ irule computeError_up
   \\ irule contained_leq_maxAbs
   \\ gs[contained_def] \\ conj_tac \\ irule REAL_LE_TRANS
-  >- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+  >- (asm_exists_tac \\ gs[] \\ irule SQRT_MONO_LE \\ real_prove)
   \\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
-  \\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC
+  \\ irule SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC
 QED
 
 (**
@@ -2440,7 +2440,10 @@ Proof
              by (
             inversion `eval_expr E1 _ (Unop Sqrt _) _ _` eval_expr_cases \\ fs[]
             \\ Cases_on ‘m1'’ \\ gs[isCompat_def, perturb_def]
-            \\ imp_res_tac meps_0_deterministic \\ gs[])
+            \\ ‘v1'' = v1’ suffices_by gs[]
+            \\ irule meps_0_deterministic
+            \\ qexistsl_tac [‘E1’, ‘λ e. FloverMapTree_find e Gamma’, ‘e’]
+            \\ gs[])
           \\ rveq \\ gs[])
       >- simp[Once validErrorbound_def]
       \\ irule Unop_sqrt' \\ fsrw_tac [SATISFY_ss] [updDefVars_def]
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index 8428a2cf8fbbb0856ab26c829be52e7fa6c1926e..e966341aa18ff56c552a0029f118e7ef5048cfaa 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -808,7 +808,7 @@ Proof
       \\ fs[perturb_def, evalUnop_def]
       \\ fs[REAL_INV_1OVER, mTypeToR_def, isCompat_def, minExponentPos_def])
     (* sqrt 0 *)
-    \\ ‘0 < sqrt (float_to_real (fp64_to_float v))’ by (irule transcTheory.SQRT_POS_LT \\ gs[])
+    \\ ‘0 < sqrt (float_to_real (fp64_to_float v))’ by (irule SQRT_POS_LT \\ gs[])
     \\ gs[evalUnop_def])
   >- (
     rename1 `Binop b (toRExp e1) (toRExp e2)` \\ rveq
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 3419d12a6a7c2a008da83c8ef66e6422c34915eb..7dd1cce457e15c1e262db48c1119a88f16cad1da 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -280,7 +280,7 @@ Theorem iv_sqrt_preserves_valid:
     0 ≤ IVlo iv ∧ valid iv ⇒ valid (sqrtInterval iv)
 Proof
   gs[valid_def, sqrtInterval_def] \\ rpt strip_tac
-  \\ irule transcTheory.SQRT_MONO_LE \\ gs[]
+  \\ irule SQRT_MONO_LE \\ gs[]
 QED
 
 val interval_addition_valid = store_thm ("interval_addition_valid",
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 62c342676294460b3886a42adfa202c8520af23d..74652b5653adfbb5759d857a6aad3661cb5651fc 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -282,10 +282,10 @@ Proof
       >- (
          irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
          \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
-         \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+         \\ irule SQRT_MONO_LE \\ real_prove)
       \\ irule REAL_LE_TRANS \\ qexists_tac ‘sqrt (SND iv)’ \\ conj_tac
       >- (
-        irule transcTheory.SQRT_MONO_LE \\ gs[]
+        irule SQRT_MONO_LE \\ gs[]
         \\ irule REAL_LE_TRANS \\ qexists_tac ‘FST iv’ \\ real_prove)
       \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[])
   (* Binary operator case *)
@@ -559,7 +559,7 @@ Proof
       \\ strip_tac
       \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
       \\ irule REAL_LE_TRANS \\ qexists_tac ‘sqrt(SND iv)’\\ gs[]
-      \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+      \\ irule SQRT_MONO_LE \\ real_prove)
   >- (rename1 `Binop b f1 f2`
       \\ rpt (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[])
       \\ rveq \\ fs[]
diff --git a/hol4/sqrtApproxScript.sml b/hol4/sqrtApproxScript.sml
index cec97a1908e451b4c7bd9b8cde9a756af1388440..d15f2768d4ecd9f7f4449e52ff38ebfc44bc69a4 100644
--- a/hol4/sqrtApproxScript.sml
+++ b/hol4/sqrtApproxScript.sml
@@ -3,22 +3,6 @@ open preambleFloVer;
 
 val _ = new_theory "sqrtApprox";
 
-(*
-Definition newton_helper_def:
-  newton_helper 0 n (x:real) = x ∧
-  newton_helper (SUC n) (init:real) x = newton_helper n init ((x + (init / x)) / 2)
-End
-
-Definition newton_def:
-  newton (n:num) (x:real) = newton_helper n x x
-End
-
-Definition newton_def:
-  newton 0 n (x:real) = x ∧
-  newton (SUC n) m x = newton n m ((x + (&m / x)) / 2)
-End
-*)
-
 Definition newton_def:
   newton 0 n (x:real) = x ∧
   newton (SUC n) (m:real) x = newton n m ((x + (m / x)) / 2)