src/HOL/Analysis/Retracts.thy
changeset 72943 b945880827ff
parent 72490 df988eac234e
child 73932 fd21b4a93043
equal deleted inserted replaced
72942:8b92a2ab5370 72943:b945880827ff