src/HOL/ex/Hilbert_Classical.thy
changeset 38256 d2f094d97c91
parent 32960 69916a850301