doc-src/Tutorial/ToyList/inductxs
author oheimb
Thu, 15 Feb 2001 16:00:44 +0100
changeset 11138 bdfb9ec76a0a
parent 5377 efb799c5ed3c
permissions -rw-r--r--
simplified proof of Least_mono

by(induct_tac "xs" 1);