src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 63728 4e078ae3682c
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75