src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 69096 62a0d10386c1
parent 69064 5840724b1d71
child 69260 0a9688695a1b