src/HOL/ex/Hilbert_Classical.thy
changeset 26898 0fffc7bc3604
parent 26828 60d1fa8e0831
child 32960 69916a850301