Hi Michael, thanks for fixing the bugs. (now I see why I can’t find its definition…)
Going in this direction, have you considered adding also “Lemma” and “Corollary”? Internally they're equivalent with “Theorem”, but they could literally help writers (and readers) identifying different levels of theorems, like those in math books. —Chun > Il giorno 02 gen 2019, alle ore 15:44, <michael.norr...@data61.csiro.au> > <michael.norr...@data61.csiro.au> ha scritto: > > 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
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
