Thanks, Konrad! Could you check to see if the HOL4 method of proving the IN_*
theorems is simpler than the HOL Light method? If it isn't, then maybe I
should be satisfied with what I came up with,following sets.ml
let IN_Interval = prove
(`! A B X. X IN open (A,B) <=> Between A X B`,
REWRITE_TAC[IN_ELIM_THM; Interval_DEF]);;
Michael, I'm finding the Logic manual to be far more illuminating than the
Stanford links in thewiki page on Type. I see my problem: Russell & Whitehead
foundationalized math using types, but Z&F also did it using sets, and
mathematicians only learn about the ZFC way, and not the earlier type way. I
think I'm an expert on the Lambda calculus (paper on my web page), and I knew
there is a typed LC, but I had no idea that Church worked on anything like set
theory. And yet he did, and I need to learn it!
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
