src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 71236 6c1ed478605e
parent 71172 575b3a818de5
child 71629 2e8f861d21d4