src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 80182 29f2b8ff84f3
parent 80095 0f9cd1a5edbe
child 82323 b022c013b04b