src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 66230 ae814012b95f
parent 66089 def95e0bc529
child 66447 a1f5c5c26fa6
equal deleted inserted replaced
66229:d3b6e5e47015 66230:ae814012b95f