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 ``antisymmetric Z`` is redundant by:
|- ∀Z. transitive Z ∧ irreflexive Z ⇒ antisymmetric Z
So the definition would better correspond to the theorem:
|- ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ transitive Z
Paul
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure contains a
definitive record of customers, application performance, security
threats, fraudulent activity and more. Splunk takes this data and makes
sense of it. Business sense. IT sense. Common sense.
http://p.sf.net/sfu/splunk-d2dcopy1
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
