src/HOL/Hilbert_Choice.thy
changeset 75734 7671f9fc66d7
parent 75607 3c544d64c218
child 80760 be8c0e039a5e
equal deleted inserted replaced
75733:d3430f302c2e 75734:7671f9fc66d7