src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 66384 cc66710c9d48
parent 66089 def95e0bc529
child 66447 a1f5c5c26fa6