src/HOL/Real/HahnBanach/Linearform.thy
changeset 24604 d5c5d2e13fbf
parent 23378 1d138d6bb461
child 25762 c03e9d04b3e4