indrule.ML
Fri, 25 Nov 1994 16:24:18 +0100 wenzelm minor changes according to new hologic;
Wed, 12 Oct 1994 12:00:45 +0100 lcp {HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
Thu, 08 Sep 1994 11:01:45 +0200 lcp {HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
Tue, 06 Sep 1994 13:24:29 +0200 lcp corrected comment re treatment of types such as (bool*bool)*bool
Thu, 25 Aug 1994 11:01:45 +0200 lcp INSTALLATION OF INDUCTIVE DEFINITIONS
less more (0) tip