On Wed, Sep 28, 2011 at 11:11 PM, Paul Loewenstein wrote:
>
> I'm back on HOL after more than a decade-long hiatus. How it's improved!
Lots more automation than back in the day. Also lots more theories and
examples.
Konrad.
--
On 29/09/11 14:11, Paul Loewenstein wrote:
>
> I'm back on HOL after more than a decade-long hiatus. How it's improved!
That's good to hear!
> I never thought I would want to take issue after just a few hours of use:
>
> In relationTheory, StrongOrder is defined as:
>
> |- ∀Z. StrongOrder
I'm back on HOL after more than a decade-long hiatus. How it's improved!
I never thought I would want to take issue after just a few hours of use:
In relationTheory, StrongOrder is defined as:
|- ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ antisymmetric Z ∧ transitive Z
However, the term ``antisy
