doc-src/Tutorial/ToyList/inductxs
author wenzelm
Fri, 16 Apr 1999 14:49:09 +0200
changeset 6439 7eea9f25dc49
parent 5377 efb799c5ed3c
permissions -rw-r--r--
'HOL/recdef' theory data;

by(induct_tac "xs" 1);