isabelle: Changelog

paulson [Tue, 22 Apr 1997 11:45:22 +0200] rev 3008

Ran expandshort

wenzelm [Tue, 22 Apr 1997 11:37:12 +0200] rev 3007

removed -norc;

wenzelm [Tue, 22 Apr 1997 11:25:45 +0200] rev 3006

tuned;

nipkow [Mon, 21 Apr 1997 13:49:40 +0200] rev 3005

Modified credits.

paulson [Mon, 21 Apr 1997 12:16:29 +0200] rev 3004

New elimination rule for "unique existence"

paulson [Mon, 21 Apr 1997 12:16:04 +0200] rev 3003

New introduction rule for "unique existence"

paulson [Mon, 21 Apr 1997 11:19:28 +0200] rev 3002

Reorganized under headings. Also documented Blast_tac and LFilter

paulson [Mon, 21 Apr 1997 10:38:46 +0200] rev 3001

Tidied up the indentation

paulson [Mon, 21 Apr 1997 10:16:41 +0200] rev 3000

Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML

paulson [Mon, 21 Apr 1997 10:16:01 +0200] rev 2999

Penalty for branching instantiations reduced from log3 to log4. Now allows a branch to close by unifying an OConst with a Const.

isabelle