src/HOL/Hilbert_Choice.thy
changeset 68955 0851db8cde12
parent 68802 3974935e0252
child 68975 5ce4d117cea7