Skip to content
Success

Changes

Summary

  1. Lukas Steven's more general fold foctions for maps
  2. More general fold function for maps
Changeset 73833:ae2f8144b60d by nipkow:
Lukas Steven's more general fold foctions for maps
Changeset 73832:9db620f007fa by nipkow:
More general fold function for maps
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/AList.thy (diff)
The file was modified src/HOL/Library/AList_Mapping.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Finite_Lattice.thy (diff)
The file was modified src/HOL/Library/Mapping.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/RBT.thy (diff)
The file was modified src/HOL/Library/RBT_Mapping.thy (diff)
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Map.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)