src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 82255 8a01d2ed484e
parent 81097 6c81cdca5b82
equal deleted inserted replaced
82254:8183a7d8a695 82255:8a01d2ed484e