src/HOL/Hilbert_Choice.thy
changeset 26479 3a2efce3e992
parent 26347 105f55201077
child 26562 9d25ef112cf6