src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 67277 7dda4a667e40
parent 67226 ec32cdaab97b
child 67399 eab6ce8368fa
equal deleted inserted replaced
67276:abac35ee3565 67277:7dda4a667e40