doc-src/Tutorial/Ifexpr/norm.ML
author wenzelm
Tue, 25 Jan 2000 22:31:53 +0100
changeset 8143 b0e44ab73631
parent 5377 efb799c5ed3c
permissions -rw-r--r--
added map, map_st;

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