Some fixes

- Unicode violations - Missing `INCLUDES` in `Holmakefile` - Update a `README`
HOL-Theorem-Prover · Mar 26, 2024 · b53822e · b53822e
1 parent f57070d
commit b53822e
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 8 deletions.
diff --git a/examples/cv_compute/Holmakefile b/examples/cv_compute/Holmakefile
@@ -1 +1,2 @@
-INCLUDES = $(HOLDIR)/examples/bootstrap
+INCLUDES = $(HOLDIR)/src/num/theories/cv_compute/automation/ \
+           $(HOLDIR)/examples/bootstrap
diff --git a/examples/cv_compute/README b/examples/cv_compute/README
@@ -5,8 +5,9 @@ Examples on using the cv_computeLib library
 
    examplesScript.sml      Two examples of how to define functions in the :cv
                            type, for use with cv_computeLib.compute.
-   cv_numsLib.{sig,sml}    An example building a conversion for natural number
-                           arithmetic using cv_computeLib.
-   cv_numsScript.sml       Support theorems and definitions for cv_numsLib.
-   cv_numsTestScript.sml   Examples using cv_numsLib.
 
+   cv_golScript.sml        An example which uses cv_transLib to evaluate
+                           Conway's Game of Life symbolically.
+
+   cv_bootScript.sml       An example which applies cv_transLib to the compiler
+                           from HOL/examples/bootstrap.
diff --git a/src/finite_maps/sptreeScript.sml b/src/finite_maps/sptreeScript.sml
@@ -426,7 +426,7 @@ Proof
 QED
 
 Theorem lrnext_eq:
-  ∀n. sptree$lrnext n = 2 ** (LOG 2 (n + 1))
+  !n. sptree$lrnext n = 2 ** (LOG 2 (n + 1))
 Proof
   strip_tac >> completeInduct_on `n` >> rw[] >>
   rw[Once lrnext_def] >>

diff --git a/src/n-bit/bitstringScript.sml b/src/n-bit/bitstringScript.sml
@@ -833,13 +833,13 @@ Proof
   simp[word_lsl_v2w, word_lsr_v2w, rotate_def, word_or_v2w] >>
   simp[Once v2w_11] >> simp[field_def, arithmeticTheory.ADD1] >>
   `shiftr v 0 = v` by simp[shiftr_def] >> simp[] >>
-  `¬ (LENGTH v < r MOD LENGTH v)` by (
+  `~(LENGTH v < r MOD LENGTH v)` by (
     simp[arithmeticTheory.NOT_LESS] >>
     irule arithmeticTheory.LESS_IMP_LESS_OR_EQ >>
     simp[arithmeticTheory.MOD_LESS]) >>
   rewrite_tac[fixwidth] >> simp[length_shiftr] >>
   qmatch_goalsub_abbrev_tac `bor a b` >>
-  `¬ (LENGTH (bor a b) < LENGTH v)` by (
+  `~(LENGTH (bor a b) < LENGTH v)` by (
     unabbrev_all_tac >> rewrite_tac[bor_def, bitwise_def] >>
     simp[length_shiftr, shiftl_def, length_fixwidth, length_pad_right]) >>
   unabbrev_all_tac >>