src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 68031 eda52f4cd4e4
parent 67685 bdff8bf0a75b
child 68072 493b818e8e10