From adc733eac3cce0b29c0005fde1f7111638ee6cd7 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Tue, 4 Jul 2023 13:47:29 +1000
Subject: [PATCH] Fix a proof broken by changes in HOL master

---
 misc/byteScript.sml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/misc/byteScript.sml b/misc/byteScript.sml
index 6748296134..7e58e97217 100644
--- a/misc/byteScript.sml
+++ b/misc/byteScript.sml
@@ -159,8 +159,6 @@ Proof
     \\ qexists_tac`2 ** dimindex(:'a)`
     \\ simp[X_LT_EXP_X] )
   \\ simp[words_of_bytes_def]
-  \\ conj_tac
-  >- ( DEP_REWRITE_TAC[ZERO_DIV] \\ fs[] )
   \\ rw[ADD1]
   \\ `MAX 1 (w2n (bytes_in_word:'a word)) = w2n (bytes_in_word:'a word)`
       by rw[MAX_DEF]