src/HOL/Analysis/Retracts.thy
changeset 79268 154166613b40
parent 78336 6bae28577994
child 79669 a3e7a323780f