src/HOL/Analysis/Retracts.thy
changeset 71606 b3b0d87edd20
parent 71193 777d673fa672
child 72490 df988eac234e