src/HOL/HahnBanach/FunctionNorm.thy
changeset 31794 71af1fd6a5e4
parent 29291 d3cc5398bad5
equal deleted inserted replaced
31793:7c10b13d49fe 31794:71af1fd6a5e4