remove another obsolete lemma

CakeML · Feb 17, 2021 · dd7aa9e · dd7aa9e
1 parent ab35dba
commit dd7aa9e
Showing 1 changed file with 0 additions and 8 deletions.
diff --git a/candle/overloading/syntax/holSyntaxCyclicityScript.sml b/candle/overloading/syntax/holSyntaxCyclicityScript.sml
@@ -3544,14 +3544,6 @@ Definition infin_or_leq_def:
     (~LFINITE ll \/ (LFINITE ll /\ k <= THE (LLENGTH ll) /\ P))
 End
 
-(*
-Theorem not_infin_or_leq[simp]:
-  !ll k. ~infin_or_leq ll (SUC k) T = (LFINITE ll /\ THE (LLENGTH ll) <= k)
-Proof
-  rw[infin_or_leq_def,EQ_IMP_THM,NOT_LESS]
-QED
-*)
-
 Theorem LNTH_EL_LTAKE:
   !ll n k.
   infin_or_leq ll k T /\ n < k ==> LNTH n ll = SOME (EL n (THE (LTAKE k ll)))