summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesTheory.sig
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/primitivesTheory.sig')
-rw-r--r--backends/hol4/primitivesTheory.sig5
1 files changed, 0 insertions, 5 deletions
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 23846737..583f66bd 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -190,7 +190,6 @@ sig
val i8_sub_eq : thm
val index_update_diff : thm
val index_update_same : thm
- val int_of_num_neq_inj : thm
val isize_add_eq : thm
val isize_div_eq : thm
val isize_mul_eq : thm
@@ -1320,10 +1319,6 @@ sig
j ≠ i ⇒
index j (update ls i y) = index j ls
- [int_of_num_neq_inj] Theorem
-
- ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m
-
[isize_add_eq] Theorem
[oracles: DISK_THM]