Further fixes for rename of material in src/ring/src

Includes first steps towards changing names of corresponding OpenTheory material though this is not yet finished.
HOL-Theorem-Prover · Jul 20, 2023 · 2546673 · 2546673
1 parent 8f595ca
commit 2546673
Show file tree

Hide file tree

Showing 9 changed files with 78 additions and 38 deletions.
diff --git a/src/rational/ratLib.sml b/src/rational/ratLib.sml
@@ -435,7 +435,7 @@ val RAT_ELIMINATE_MINV_TAC = CONV_TAC RAT_ELIMINATE_MINV_CONV;
 (* rewrites to calculate operations on integers
    (TODO) remove dependencies: numRingTheory and integerRingTheory
  *)
-local open numeralTheory numRingTheory integerRingTheory in
+local open numeralTheory EVAL_numRingTheory integerRingTheory in
 
 val num_rewrites =
    [numeral_distrib, numeral_eq, numeral_suc, numeral_iisuc, numeral_add,

diff --git a/src/ring/src/quote.otd → src/ring/src/EVAL_quote.otd b/src/ring/src/quote.otd → src/ring/src/EVAL_quote.otd
diff --git a/src/ring/src/ring.otd → src/ring/src/EVAL_ring.otd b/src/ring/src/ring.otd → src/ring/src/EVAL_ring.otd
diff --git a/src/ring/src/ringNorm.otd → src/ring/src/EVAL_ringNorm.otd b/src/ring/src/ringNorm.otd → src/ring/src/EVAL_ringNorm.otd
diff --git a/src/ring/src/semi_ring.otd → src/ring/src/EVAL_semiring.otd b/src/ring/src/semi_ring.otd → src/ring/src/EVAL_semiring.otd
diff --git a/src/ring/src/Holmakefile b/src/ring/src/Holmakefile
@@ -6,16 +6,16 @@ ifeq ($(KERNELID),otknl)
 ARTFILES = $(patsubst %Script.sml,%.ot.art,$(wildcard *Script.sml))
 all: $(ARTFILES) hol4-ring.art
 
-ring.art: ring.otd
-semi_ring.art: semi_ring.otd
-quote.art: quote.otd
-canonical.art: canonical.otd
-ringNorm.art: ringNorm.otd
+EVAL_ring.art: EVAL_ring.otd
+EVAL_semi_ring.art: EVAL_semi_ring.otd
+EVAL_quote.art: EVAL_quote.otd
+EVAL_canonical.art: EVAL_canonical.otd
+EVAL_ringNorm.art: EVAL_ringNorm.otd
 
-hol4-ring-unint.art: hol4-ring-unint.thy $(ARTFILES)
+hol4-ring-unint.art: hol4-eval-ring-unint.thy $(ARTFILES)
 	opentheory info --article -o $@ $<
 
-hol4-ring.art: hol4-ring.thy hol4-ring-unint.art ../../opentheory/hol4.int
+hol4-ring.art: hol4-eval-ring.thy hol4-eval-ring-unint.art ../../opentheory/hol4.int
 	opentheory info --article -o $@ $<
 
 install: hol4-ring.thy hol4-ring.art

diff --git a/src/ring/src/hol4-eval-ring-unint.thy b/src/ring/src/hol4-eval-ring-unint.thy
@@ -0,0 +1,40 @@
+name: hol-eval-ring-unint
+version: 1.1
+description: HOL ring theories (before re-interpretation)
+author: HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
+license: MIT
+main {
+  import: EVAL_ring
+  import: EVAL_canonical
+  import: EVAL_numring
+  import: EVAL_quote
+  import: EVAL_ring-norm
+  import: EVAL_semiring
+}
+EVAL_ring {
+  import: EVAL_semiring
+  article: "EVAL_ring.ot.art"
+}
+EVAL_ring-norm {
+  import: EVAL_canonical
+  import: EVAL_ring
+  import: EVAL_semiring
+  article: "EVAL_ringNorm.ot.art"
+}
+EVAL_canonical {
+  import: EVAL_quote
+  import: EVAL_semiring
+  article: "EVAL_canonical.ot.art"
+}
+EVAL_quote {
+  article: "EVAL_quote.ot.art"
+}
+EVAL_semiring {
+  article: "EVAL_semiring.ot.art"
+}
+EVAL_numring {
+  import: EVAL_canonical
+  import: EVAL_quote
+  import: EVAL_semiring
+  article: "EVAL_numRing.ot.art"
+}
diff --git a/src/ring/src/hol4-ring.thy → src/ring/src/hol4-eval-ring.thy b/src/ring/src/hol4-ring.thy → src/ring/src/hol4-eval-ring.thy
@@ -1,4 +1,4 @@
-name: hol-ring
+name: hol-eval-ring
 version: 1.2
 description: HOL ring theories
 author: HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
@@ -14,6 +14,6 @@ show: "Function"
 show: "Number.Natural"
 show: "Relation"
 main {
-  article: "hol4-ring-unint.art"
+  article: "hol4-ring-eval-unint.art"
   interpretation: "../../opentheory/hol4.int"
 }
diff --git a/src/ring/src/hol4-ring-unint.thy b/src/ring/src/hol4-ring-unint.thy
@@ -1,40 +1,40 @@
-name: hol-ring-unint
+name: hol-eval-ring-unint
 version: 1.1
 description: HOL ring theories (before re-interpretation)
 author: HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
 license: MIT
 main {
-  import: ring
-  import: canonical
-  import: num-ring
-  import: quote
-  import: ring-norm
-  import: semi-ring
+  import: EVAL_ring
+  import: EVAL_canonical
+  import: EVAL_numring
+  import: EVAL_quote
+  import: EVAL_ring-norm
+  import: EVAL_semiring
 }
-ring {
-  import: semi-ring
-  article: "ring.ot.art"
+EVAL_ring {
+  import: EVAL_semiring
+  article: "EVAL_ring.ot.art"
 }
-ring-norm {
-  import: canonical
-  import: ring
-  import: semi-ring
-  article: "ringNorm.ot.art"
+EVAL_ring-norm {
+  import: EVAL_canonical
+  import: EVAL_ring
+  import: EVAL_semiring
+  article: "EVAL_ringNorm.ot.art"
 }
-canonical {
-  import: quote
-  import: semi-ring
-  article: "canonical.ot.art"
+EVAL_canonical {
+  import: EVAL_quote
+  import: EVAL_semiring
+  article: "EVAL_canonical.ot.art"
 }
-quote {
-  article: "quote.ot.art"
+EVAL_quote {
+  article: "EVAL_quote.ot.art"
 }
-semi-ring {
-  article: "semi_ring.ot.art"
+EVAL_semiring {
+  article: "EVAL_semiring.ot.art"
 }
-num-ring {
-  import: canonical
-  import: quote
-  import: semi-ring
-  article: "numRing.ot.art"
+EVAL_numring {
+  import: EVAL_canonical
+  import: EVAL_quote
+  import: EVAL_semiring
+  article: "EVAL_numRing.ot.art"
 }