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 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 > Good point. I've made this change in the repository. See https://github.com/mn200/HOL/commit/5204b7f7993f2963fea7b6fcea769c60c4bffb5a Thanks for the suggestion! Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
