src/HOL/Real/HahnBanach/Linearform.thy
changeset 29140 e7ac5bb20aed
parent 27612 d3eb431db035
child 29234 60f7fb56f8cd