<div dir="ltr"><div><div><div>Cezary Kaliszyk and Alexander Krauss have done a lovely piece of work that was just presented at ITP 2013 (<a href="http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf">http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf</a>) about efficient import from HOL Light into Isabelle/HOL.<br>

<br></div>Their approach has many similarities to OpenTheory, and their proof trace format is not too different from OpenTheory article format, and indeed in Alex's talk he said integration with OpenTheory would be a worthy goal.<br>

<br></div>The performance of their method is very impressive, and certainly faster than using OpenTheory as it is now, so I think it would greatly benefit OpenTheory to adopt and standardise K&K's ideas.<br><br>I write this message to ask OpenTheory users for their comments on this proposal, and to make a call for volunteers to help with the integration/adoption. As a first step, perhaps we could just make a list of the differences from how OpenTheory currently works, to see what needs to be done.<br>

<br></div>Ramana<br></div>