John, thanks for your responses! It's a great pleasure to be logged in at the same time as you (because my wife is on vacation). I think I can largely solve my locale/axiom problems by using HOL, which I just started learning about, in the sets section of your tutorial.
Thanks for correcting me, that was really dumb of me. This works fine: parse_as_prefix "elt_inv";; let left_inv = new_axiom `!x . (left_inv x) prod x = unit`;; Or even this, although I don't understand the priority biz: let left_inv = new_axiom `!x . left_inv x prod x = unit`;; I should have guessed the lambda_calculus connection maybe, and did I tell you I wrote a paper on the lambda_calculus, http://www.math.northwestern.edu/~richter/lambda-calc.pdf giving a simpler proof than Barendregt's of the Standard Reduction Theorem in the Lambda Calculus, which explains in what sense the Lambda Calculus is a compiler. -- 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
