doc-src/Tutorial/ToyList/inductxs
author kleing
Sat, 09 Nov 2002 00:12:25 +0100
changeset 13703 a36a0d417133
parent 5377 efb799c5ed3c
permissions -rw-r--r--
Hoare.ML -> hoare.ML

by(induct_tac "xs" 1);