Remove uses of load, which is forbidden under mosml

HOL-Theorem-Prover · Nov 8, 2023 · ee74295 · ee74295
1 parent 52721c8
commit ee74295
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 6 deletions.
diff --git a/examples/fermat/twosq/helperTwosqScript.sml b/examples/fermat/twosq/helperTwosqScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "helperTwosq";
 
 
 (* open dependent theories *)
-val _ = load("helperFunctionTheory");
 open helperFunctionTheory;
 open helperSetTheory;
 open helperNumTheory;
@@ -24,7 +23,6 @@ open arithmeticTheory pred_setTheory;
 open dividesTheory;
 open gcdTheory; (* for GCD_IS_GREATEST_COMMON_DIVISOR *)
 
-val _ = load("logPowerTheory");
 open logPowerTheory; (* for SQRT *)
 
 open whileTheory; (* for HOARE_SPEC_DEF *)

diff --git a/examples/fermat/twosq/hoppingScript.sml b/examples/fermat/twosq/hoppingScript.sml
@@ -30,7 +30,6 @@ open helperListTheory;
 open listRangeTheory; (* for listRangeLHI_ALL_DISTINCT *)
 open indexedListsTheory; (* for findi_EL and EL_findi *)
 
-load "sublistTheory";
 open sublistTheory;
 
 open quarityTheory;

diff --git a/examples/fermat/twosq/involuteFixScript.sml b/examples/fermat/twosq/involuteFixScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "involuteFix";
 
 
 (* open dependent theories *)
-val _ = load("involuteTheory");
 open helperFunctionTheory; (* for FUNPOW_2 *)
 open helperSetTheory; (* for BIJ_ELEMENT *)
 open helperNumTheory; (* for MOD_EQ *)

diff --git a/examples/fermat/twosq/iterateComputeScript.sml b/examples/fermat/twosq/iterateComputeScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "iterateCompute";
 
 
 (* open dependent theories *)
-val _ = load("iterationTheory");
 open helperFunctionTheory;
 open helperSetTheory;
 open helperNumTheory;

diff --git a/examples/fermat/twosq/iterationScript.sml b/examples/fermat/twosq/iterationScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "iteration";
 
 
 (* open dependent theories *)
-val _ = load("helperFunctionTheory");
 (* open helperTwosqTheory; *)
 open helperFunctionTheory;
 open helperSetTheory;