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
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
