Lambda the Ultimate

A new blog entry has beed created with continues the description of Modern Eiffel's proof engine.

This blog entry focuses on the introduction of negation and it's axioms into the class BOOLEAN and presents a rich set of proofs.

This entry completes the use of the proof engine for propositional calculus. The next entries will focus more on real calculations using inductive data types.