Dear Chun,
This is indeed a new feature of the quotation filter. Its purpose is to keep
names consistent, and to reduce the amount of boilerplate typing that
script-writers have to generate.
It's as yet undocumented, but I hope to get to that soon.
Michael
On 2/1/19, 06:20, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
