src/HOL/Hilbert_Choice.thy
changeset 39214 49fc6c842d6c
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
equal deleted inserted replaced
39213:297cd703f1f0 39214:49fc6c842d6c