1997-04-22 wenzelm [Tue, 22 Apr 1997 11:37:12 +0200] rev 3007
removed -norc;
bin/isabelle bin/isatool build configure lib/Tools/changeparent lib/Tools/doc lib/Tools/expandshort lib/Tools/findlogics lib/Tools/getenv lib/Tools/installfonts lib/Tools/make lib/Tools/makeall lib/Tools/symbolinput lib/Tools/usedir lib/scripts/isa-emacs lib/scripts/isa-xterm lib/scripts/run-polyml lib/scripts/run-smlnj lib/scripts/run-smlnj-0.93 lib/scripts/ucat

1997-04-22 wenzelm [Tue, 22 Apr 1997 11:25:45 +0200] rev 3006
tuned;
NEWS

1997-04-21 nipkow [Mon, 21 Apr 1997 13:49:40 +0200] rev 3005
Modified credits.
doc-src/Logics/logics.tex

1997-04-21 paulson [Mon, 21 Apr 1997 12:16:29 +0200] rev 3004
New elimination rule for "unique existence"
src/HOL/cladata.ML

1997-04-21 paulson [Mon, 21 Apr 1997 12:16:04 +0200] rev 3003
New introduction rule for "unique existence"
src/HOL/HOL.ML

1997-04-21 paulson [Mon, 21 Apr 1997 11:19:28 +0200] rev 3002
Reorganized under headings. Also documented Blast_tac and LFilter
NEWS

1997-04-21 paulson [Mon, 21 Apr 1997 10:38:46 +0200] rev 3001
Tidied up the indentation
src/HOL/Lambda/ParRed.thy

1997-04-21 paulson [Mon, 21 Apr 1997 10:16:41 +0200] rev 3000
Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
src/ZF/ex/misc.ML src/ZF/func.ML

1997-04-21 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.
src/Provers/blast.ML

1997-04-21 paulson [Mon, 21 Apr 1997 10:15:00 +0200] rev 2998
New blast_tac demo
src/HOL/ex/set.ML