src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 67161 b762ed417ed9
parent 66933 4e06b030730c
child 67226 ec32cdaab97b