doc-src/Tutorial/Ifexpr/normal_norm.ML
author nipkow
Thu, 14 Jan 1999 13:20:02 +0100
changeset 6130 30b84ad2131d
parent 5377 efb799c5ed3c
permissions -rw-r--r--
Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.

Goal "normal(norm b)";