Skip to content
Success

Changes

Summary

  1. merged
  2. added lemma refl_lex_prod[simp]
  3. added lemmas reflI and reflD
  4. added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
  5. added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
  6. added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
  7. strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
  8. strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
  9. added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
  10. strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
  11. strengthened and renamed lemmas antisymp_less and antisymp_greater
  12. strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
  13. tuned naming
  14. added lemma asymp_on_asym_on_eq[pred_set_conv]
  15. strengthened and renamed asymp_less and asymp_greater
  16. added lemmas asym_on_subset and asymp_on_subset
  17. added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
  18. added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
Changeset 76699:0b5efc6de385 by desharna:
merged
Changeset 76698:e65a50f6c2de by desharna:
added lemma refl_lex_prod[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 76697:e19a3dbbf5de by desharna:
added lemmas reflI and reflD
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76696:b6b7f3caa74a by desharna:
added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 76695:e321569ec7a1 by desharna:
added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 76694:2f8219460ac9 by desharna:
added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 76693:0fbe27cf295a by desharna:
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76692:98880b2430ea by desharna:
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76691:0c6aa6c27ba4 by desharna:
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76690:da062f9f2e53 by desharna:
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76689:ca258cf6c977 by desharna:
strengthened and renamed lemmas antisymp_less and antisymp_greater
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76688:87e7ab6aa40b by desharna:
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76687:a84716ca8b97 by desharna:
tuned naming
The file was modified src/HOL/Relation.thy (diff)
Changeset 76686:10c4aa9eecf8 by desharna:
added lemma asymp_on_asym_on_eq[pred_set_conv]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76685:806d0b3aebaf by desharna:
strengthened and renamed asymp_less and asymp_greater
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76684:3eda063a20a4 by desharna:
added lemmas asym_on_subset and asymp_on_subset
The file was modified src/HOL/Relation.thy (diff)
Changeset 76683:cca28679bdbf by desharna:
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76682:e260dabc88e6 by desharna:
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)