src/HOL/Hilbert_Choice.thy
changeset 22383 01e90256550d
parent 21999 0cf192e489e2
child 22690 0b08f218f260
equal deleted inserted replaced
22382:dbf09db0a40d 22383:01e90256550d