diff options
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefScript.sml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml index cc745e5d..8ef99530 100644 --- a/backends/hol4/divDefScript.sml +++ b/backends/hol4/divDefScript.sml @@ -7,11 +7,7 @@ how to use it. *) -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib +open primitivesArithTheory primitivesBaseTacLib primitivesTheory primitivesLib val _ = new_theory "divDef" |