From bbe4a8b234d183e36c157dbc6b9900214e405a52 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 31 Jan 2023 18:24:47 +0100
Subject: Start working on divDefLib for diverging definitions

---
 backends/hol4/testTheory.sig | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'backends/hol4/testTheory.sig')

diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig
index c1034394..21b74a39 100644
--- a/backends/hol4/testTheory.sig
+++ b/backends/hol4/testTheory.sig
@@ -102,7 +102,6 @@ sig
     val nth_fuel_P_mono : thm
     val nth_fuel_def : thm
     val nth_fuel_ind : thm
-    val nth_fuel_least_fail_mono : thm
     val nth_fuel_least_success_mono : thm
     val nth_fuel_mono : thm
     val num2error_11 : thm
@@ -695,10 +694,6 @@ sig
                P n ls i) ⇒
             ∀v v1 v2. P v v1 v2
    
-   [nth_fuel_least_fail_mono]  Theorem
-      
-      ⊢ ∀n ls i. n < $LEAST (nth_fuel_P ls i) ⇒ nth_fuel n ls i = Loop
-   
    [nth_fuel_least_success_mono]  Theorem
       
       ⊢ ∀n ls i.
-- 
cgit v1.2.3