Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. card_0_eq ~> fcard_0_eq
  3. material from $AFP/Formula_Derivatives/FSet_More
  4. FSet is monadic
  5. finite sets are countable
  6. lift sum to finite sets
Changeset 66266:130dea8500cb by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 66265:a51e72d79670 by lars hupel _lars.hupel@mytum.de_:
card_0_eq ~> fcard_0_eq
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 66264:d516da3e7c42 by lars hupel _lars.hupel@mytum.de_:
material from $AFP/Formula_Derivatives/FSet_More
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 66263:466d8e7ed170 by lars hupel _lars.hupel@mytum.de_:
FSet is monadic
The file was modified src/HOL/Library/Monad_Syntax.thy (diff)
Changeset 66262:4a2c9d32e7aa by lars hupel _lars.hupel@mytum.de_:
finite sets are countable
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
Changeset 66261:fb6efe575c6d by lars hupel _lars.hupel@mytum.de_:
lift sum to finite sets
The file was modified src/HOL/Library/FSet.thy (diff)