doc-src/Tutorial/Ifexpr/normal_normif.ML
changeset 7159 b009afd1ace5
parent 5377 efb799c5ed3c