doc-src/Tutorial/Ifexpr/proof.ML
changeset 9924 3370f6aa3200
parent 5377 efb799c5ed3c