From dc46dbb9a01329c39673fedc195006745c365030 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Jun 2023 17:23:29 +0200
Subject: Update the HOL4 proofs for the last *release* version of HOL4

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

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

diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index d8cc4ab5..2df28a2f 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -53,7 +53,6 @@ sig
     val tree_distinct : thm
     val tree_induction : thm
     val tree_nchotomy : thm
-    val tree_size_eq : thm
   
   val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar
 (*
@@ -434,10 +433,6 @@ sig
       
       ⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n
    
-   [tree_size_eq]  Theorem
-      
-      ⊢ tree1_size f = list_size (tree_size f)
-   
    
 *)
 end
-- 
cgit v1.2.3