On 31/01/18 06:49, Yaqing Jiang wrote: > Anyone knows if there is a simple way of finding out which theorems were > actually applied?
In HOL4 you can do “set_trace "simplifier" 2;” (or an higher value) to display information about how the term is being rewritten by simpLib (it is a more general facility than “REWRITE_CONV”); with the GNU Emacs mode you can use «M-h C-s» to toggle. There is also a facility “used_rewrites” within simpLib (see “src/simp/src/simpLib.sig”). In HOL Light I do not know if there is an equivalent.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
