doc-src/Tutorial/Ifexpr/proof.ML
changeset 7707 1f4b67fdfdae
parent 5377 efb799c5ed3c