src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 13470 d2cbbad84ad3
parent 11472 d08d4e17a5f6
child 13515 a6a7025fd7e8
equal deleted inserted replaced
13469:70d8dfef587d 13470:d2cbbad84ad3