Summary
- new type for finite maps; use it in HOL-Probability
The file was added | src/HOL/Library/Finite_Map.thy |
The file was modified | src/HOL/Library/Library.thy (diff) |
The file was modified | src/HOL/Probability/Fin_Map.thy (diff) |
The file was modified | src/HOL/Probability/Projective_Limit.thy (diff) |
The file was modified | src/HOL/ROOT (diff) |