Summary
- merged
- card_0_eq ~> fcard_0_eq
- material from $AFP/Formula_Derivatives/FSet_More
- FSet is monadic
- finite sets are countable
- lift sum to finite sets
The file was modified | src/HOL/Library/FSet.thy (diff) |
The file was modified | src/HOL/Library/FSet.thy (diff) |
The file was modified | src/HOL/Library/Monad_Syntax.thy (diff) |
The file was modified | src/HOL/Library/FSet.thy (diff) |
The file was modified | src/HOL/Probability/Fin_Map.thy (diff) |
The file was modified | src/HOL/Library/FSet.thy (diff) |