src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 82140 14ab8005f490
parent 80095 0f9cd1a5edbe
child 82323 b022c013b04b