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