Hi,
Anyone knows if there is a function in HOL Light that convert terms to
strings so that I can save the term and load it the next time?
If I do string_of_term `x:num` I only got "x", but I need "x:num". If
there's none I'll make one myself anyway.
Thanks
--
The University of Edinburgh
I might need to forward the solution I got from Mark here as well:
Forwarded Message
Subject:Re: [Hol-info] Tracking lemmas used by REWRITE_CONV
Date: Wed, 31 Jan 2018 15:38:46 +
From: Mark Adams <m...@proof-technologies.com>
To: Yaqing Jiang
Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term, not
all the theorems in th1,th2,... are used.
Anyone knows if there is a simple way of finding out which theorems were
actually applied?
I know there are methods that tracking the entire dependencies of a
proven theorem,
