src/HOL/Hilbert_Choice.thy
changeset 58243 3aa25f39cd74
parent 58092 4ae52c60603a
child 58481 62bc7c79212b
equal deleted inserted replaced
58242:3fb224b61995 58243:3aa25f39cd74