src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 66149 4bf16fb7c14d
parent 66089 def95e0bc529
child 66447 a1f5c5c26fa6