Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added lemmas antisym_on_subset and antisymp_on_subset
  2. strengthened antisymp_le and antisymp_ge
  3. added lemmas antisym_onD and antisymp_onD
  4. added lemmas antisym_onI and antisymp_onI
  5. added lemma antisymp_reflcp
  6. added antisymp_on_antisym_on_eq[pred_set_conv]
  7. added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
Changeset 76642:878ed0fcb510 by desharna:
added lemmas antisym_on_subset and antisymp_on_subset
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76641:e9f3f2b0c0a7 by desharna:
strengthened antisymp_le and antisymp_ge
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76640:8eb23d34323b by desharna:
added lemmas antisym_onD and antisymp_onD
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76639:e322abb912af by desharna:
added lemmas antisym_onI and antisymp_onI
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76638:d8ca2d0e81e5 by desharna:
added lemma antisymp_reflcp
The file was modified NEWS (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
Changeset 76637:6b75499e52d1 by desharna:
added antisymp_on_antisym_on_eq[pred_set_conv]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76636:e772c8e6edd0 by desharna:
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)