doc-src/Tutorial/Misc/exhaust.ML
author schirmer
Mon, 26 Jan 2004 15:33:51 +0100
changeset 14362 b378b6faf4a7
parent 9255 2ceb11a2e190
permissions -rw-r--r--
\\<...> will be converted to \<...> \\<^...> will be converted to \<^...>

Goal "(case xs of [] => [] | y#ys => xs) = xs";
by(case_tac "xs" 1);