This looks great, Vincent.
Are you interested in working on a version for HOL4?
On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com wrote:
Hi list,
I developed a new tactic that takes a theorem of the form P == l = r and
replaces l by r in a goal adding
Hi Ramana,
I will make a few performance improvements on the HOL Light version in the
coming weeks hopefully, and then I plan indeed to translate it to HOL4.
V.
2013/7/30 Ramana Kumar ramana.ku...@cl.cam.ac.uk
This looks great, Vincent.
Are you interested in working on a version for HOL4?
