doc-src/Tutorial/Ifexpr/norm.ML
author wenzelm
Wed, 15 Nov 2000 19:43:42 +0100
changeset 10473 4f15b844fea6
parent 5377 efb799c5ed3c
permissions -rw-r--r--
separate rules for function/operation definitions;

Goal "valif (norm b) env = valif b env";