diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 5 |
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] |