src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 23372 0035be079bee
parent 21404 eb85850d3eb7
child 23378 1d138d6bb461
equal deleted inserted replaced
23371:ed60e560048d 23372:0035be079bee