clasohm [Wed, 02 Nov 1994 15:26:13 +0100] rev 157
added IOA files
clasohm [Wed, 02 Nov 1994 11:50:09 +0100] rev 156
added IOA to isabelle/HOL
lcp [Tue, 01 Nov 1994 11:00:45 +0100] rev 155
HOL/HOL/swap: deleted
HOL/HOL/classical: simpler proof
lcp [Mon, 31 Oct 1994 17:17:48 +0100] rev 154
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs
lcp [Thu, 13 Oct 1994 09:39:15 +0100] rev 153
HOL/HOL.ML/selectI2: new rule for descriptions
lcp [Wed, 12 Oct 1994 12:06:56 +0100] rev 152
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding
{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
lcp [Wed, 12 Oct 1994 12:00:45 +0100] rev 151
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding
{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
nipkow [Thu, 06 Oct 1994 09:36:40 +0100] rev 150
replaced some "rules" by "defs"
clasohm [Tue, 04 Oct 1994 13:00:20 +0100] rev 149
changed precedences to eliminate some ambiguities
nipkow [Wed, 28 Sep 1994 12:39:32 +0100] rev 148
moved LList* to ex