doc-src/Tutorial/Misc/splitif.ML
author wenzelm
Tue, 13 Oct 1998 14:24:35 +0200
changeset 5642 1b3e48bdbb93
parent 5377 efb799c5ed3c
permissions -rw-r--r--
PRIVATE sig parts;

by(split_tac [split_if] 1);