src/HOL/Library/Combine_PER.thy
changeset 75560 aeb797356de0
parent 74334 ead56ad40e15