doc-src/Tutorial/Datatype/trieinduct.ML
author paulson
Thu, 29 Jul 2004 12:15:53 +0200
changeset 15083 a471fd1d9961
parent 5851 15ce4c1c8313
permissions -rw-r--r--
documents for ZF-AC and ZF-Constructible

by(induct_tac "as" 1);
by(Auto_tac);