src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 79961 2b9205301ff5
parent 79566 f783490c6c99
child 80095 0f9cd1a5edbe