Thanks Makarius and Josef, and I'll take the discussion back to the Isabelle mailing list, after saying:
Like most mathematicians, I sorta understand of FOL, e.g. the proof of Goedel incompleteness theorem, but I don't have a solid practical understanding of FOL. I feel like I should. I'm only likely to understand Mizar, HOL, Isabelle/Pure+Isar by comparison to FOL. -- Best, Bill ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info