src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 63717 3b0500bd2240
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75