On Thu, 19 Jul 2012, Ramana Kumar wrote:
On Thu, Jul 19, 2012 at 5:27 PM, Tjark Weber <[email protected]> wrote:
On Fri, 2012-07-13 at 02:48 +0200, Maïssa ELLEUCH wrote:
I would ask if someone had ported some theories from Isabelle/HOL to
the HOL theorem prover.
Perhaps Sean McLaughlin's paper "An Interpretation of Isabelle/HOL in
HOL Light" (IJCAR 2006: 192-204) could serve as a starting point.
Do you know whether McLaughlin's code is available anywhere, e.g. online?
(Also, does it still work with current versions of Isabelle and HOL Light?)
As far as I know this project never reached a usable state.
Makarius------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
