src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 70045 7b6add80e3a5
parent 69939 812ce526da33
child 70065 cc89a395b5a3