src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 79025 f78ee2d48bf5
parent 78475 a5f6d2fc1b1f
child 79566 f783490c6c99