src/HOL/Analysis/Retracts.thy
changeset 80726 5f13872a33ea
parent 79669 a3e7a323780f
child 82323 b022c013b04b
equal deleted inserted replaced
80725:ea8d52d37313 80726:5f13872a33ea