src/HOL/Hilbert_Choice.thy
changeset 28072 a45e8c872dc1
parent 27760 3aa86edac080
child 29655 ac31940cfb69
equal deleted inserted replaced
28071:6ab5b4595f64 28072:a45e8c872dc1