src/HOL/Analysis/Retracts.thy
changeset 79346 f86c310327df
parent 78336 6bae28577994
child 79669 a3e7a323780f