Hi, (Happy New Year) I found the following code in src/patricia/sptreeScript.sml (added in commit 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)
Theorem list_to_num_set_append `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) (list_to_num_set l2)` (Induct \\ rw[list_to_num_set_def] \\ rw[Once insert_union] \\ rw[Once insert_union,SimpRHS] \\ rw[union_assoc]); Where is the definition of the keyword “Theorem”? Is this a new grammar of defining theroems, aiming at preventing inconsistent theorem names in exported theories? Regards, Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
