src/HOL/Hilbert_Choice.thy
changeset 63319 bc8793d7bd21
parent 63040 eb4ddd18d635
child 63365 5340fb6633d0