src/HOL/Hilbert_Choice.thy
changeset 26479 3a2efce3e992
parent 26347 105f55201077
child 26562 9d25ef112cf6
equal deleted inserted replaced
26478:9d1029ce0e13 26479:3a2efce3e992