src/HOL/Hilbert_Choice.thy
changeset 60828 e9e272fa8daf
parent 60758 d8d85a8172b5
child 60974 6a6f15d8fbc4