src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 21964 df2e82888a66
parent 21404 eb85850d3eb7
child 23378 1d138d6bb461