doc-src/Tutorial/Ifexpr/normal_normif.ML
author wenzelm
Thu, 08 Aug 2002 23:51:24 +0200
changeset 13486 54464ea94d6f
parent 5377 efb799c5ed3c
permissions -rw-r--r--
exception SIMPROC_FAIL: solid error reporting of simprocs;

Goal "!t e. normal(normif b t e) = (normal t & normal e)";