src/HOL/Hilbert_Choice.thy
changeset 63421 3bf02e7fa8a3
parent 63374 1a474286f315
child 63540 f8652d0534fa
equal deleted inserted replaced
63420:b43a3f7d9935 63421:3bf02e7fa8a3