Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element
  2. added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element
  3. refactored proofs
  4. added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element
  5. reversed import dependency between Relation and Finite_Set; and move theorems around
Changeset 77699:d5060a919b3f by desharna:
reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 77698:51ed312cabeb by desharna:
added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element
The file was modified NEWS (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
Changeset 77697:f35cbb4da88a by desharna:
refactored proofs
The file was modified src/HOL/Finite_Set.thy (diff)
Changeset 77696:9c7cbad50e04 by desharna:
added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element
The file was modified NEWS (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
Changeset 77695:93531ba2c784 by desharna:
reversed import dependency between Relation and Finite_Set; and move theorems around
The file was modified NEWS (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)