doc-src/Tutorial/Ifexpr/normal_norm.ML
author wenzelm
Fri, 04 Jun 1999 19:55:41 +0200
changeset 6778 2f66eea8a025
parent 5377 efb799c5ed3c
permissions -rw-r--r--
Support for calculational proofs.

Goal "normal(norm b)";