Hi Thomas, Perfect! Thanks very much! This is exactly what I needed.
Regards, Chun > Il giorno 05 mag 2017, alle ore 22:15, Thomas Tuerk <tho...@tuerk-brechen.de> > ha scritto: > > Hi, > > I always understood "fail" as raising "HOL_ERR". However, I might be wrong > there. > > There is QCONV. If a conversion raises UNCHANGED, it calls REFL. So > > QCONV (REWRITE_CONV thms) > > is what you are after, I believe. > Thomas > > On 05.05.2017 22:09, Chun Tian (binghe) wrote: >> Hi, >> >> The HOL System REFERENCE said, REWRITE_CONV "Does not fail, but may diverge >> if the sequence of rewrites is non-terminating.”, but I found this is not >> true (any more): >> >> >>> REWRITE_CONV [ASSUME ``A = B``] ``A``; >>> >> val it = >> [.] |- A = B: >> thm >> >>> REWRITE_CONV [ASSUME ``A = B``] ``C``; >>> >> Exception- UNCHANGED raised >> >> What I wanted is a theorem ``C = C`` in this case. >> >> Further more, >> >> >>> REWRITE_CONV [] ``F`` >>> >> Exception- UNCHANGED raised >> >> which used to return a theorem ``F = F`` in HOL88: >> >> #REWRITE_CONV [] "F";; >> |- F = F >> >> Is there a way I could get the desired (old) behavior? >> >> Regards, >> >> Chun Tian >> >> >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! >> http://sdm.link/slashdot >> >> >> _______________________________________________ >> hol-info mailing list >> >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! > http://sdm.link/slashdot_______________________________________________ > 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
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
