[Hol-info] New grammar of defining theorems?

[Chun T. (binghe) <bin...@gm...>]

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