src/HOL/Hilbert_Choice.thy
changeset 29140 e7ac5bb20aed
parent 27760 3aa86edac080
child 29655 ac31940cfb69
equal deleted inserted replaced
29139:6e0b7b114072 29140:e7ac5bb20aed