I see… thanks, but currently Moscow ML cannot compile that file [1], and I can’t even find the definition of this new feature …
—Chun [1] https://github.com/HOL-Theorem-Prover/HOL/pull/634 > 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
