From df4d60b71bcabf9897656d6d74157a4c7d8d539c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 16 May 2023 11:45:43 +0200
Subject: Make good progress on generating code for HOL4

---
 backends/hol4/divDefLibTestScript.sml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'backends/hol4/divDefLibTestScript.sml')

diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml
index 80170b24..f5df6139 100644
--- a/backends/hol4/divDefLibTestScript.sml
+++ b/backends/hol4/divDefLibTestScript.sml
@@ -1,11 +1,6 @@
 (* Examples which use divDefLib.DefineDiv *)
 
-open HolKernel boolLib bossLib Parse
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-open divDefTheory divDefLib
+open primitivesLib divDefLib
 
 val _ = new_theory "divDefLibTest"
 
-- 
cgit v1.2.3