doc-src/Tutorial/Datatype/trieexhaust.ML
author paulson
Thu, 06 Jul 2000 15:01:52 +0200
changeset 9266 1b917b8b1b38
parent 9255 2ceb11a2e190
permissions -rw-r--r--
removal of batch style, and tidying

by(ALLGOALS (case_tac "bs"));