src/HOL/Real/HahnBanach/Linearform.thy
changeset 17411 664434175578
parent 16417 9bc16273c2d4
child 23378 1d138d6bb461