1997-05-06 wenzelm [Tue, 06 May 1997 12:51:23 +0200] rev 3109
added \Pure, \CPure;
doc-src/iman.sty

1997-05-06 wenzelm [Tue, 06 May 1997 12:50:16 +0200] rev 3108
misc updates, tuning, cleanup;
doc-src/Ref/classical.tex doc-src/Ref/defining.tex doc-src/Ref/goals.tex doc-src/Ref/introduction.tex doc-src/Ref/ref.ind doc-src/Ref/ref.rao doc-src/Ref/ref.tex doc-src/Ref/simplifier.tex doc-src/Ref/substitution.tex doc-src/Ref/syntax.tex doc-src/Ref/tactic.tex doc-src/Ref/tctical.tex doc-src/Ref/theories.tex doc-src/Ref/theory-syntax.tex doc-src/Ref/thm.tex

1997-05-05 wenzelm [Mon, 05 May 1997 21:18:01 +0200] rev 3107
tuned;
NEWS

1997-05-05 wenzelm [Mon, 05 May 1997 18:50:26 +0200] rev 3106
tuned;
doc-src/Intro/advanced.tex doc-src/Intro/foundations.tex

1997-05-05 nipkow [Mon, 05 May 1997 18:09:31 +0200] rev 3105
Cosmetic update of induct_tac; test first now.
src/HOL/datatype.ML

1997-05-05 wenzelm [Mon, 05 May 1997 13:24:38 +0200] rev 3104
SYNC;
doc-src/Intro/intro.ind

1997-05-05 wenzelm [Mon, 05 May 1997 13:24:11 +0200] rev 3103
misc updates, tuning, cleanup;
doc-src/Intro/advanced.tex doc-src/Intro/foundations.tex doc-src/Intro/getting.tex

1997-05-05 paulson [Mon, 05 May 1997 12:15:53 +0200] rev 3102
Some blast_tac calls; more needed
src/HOL/Auth/Message.ML src/HOL/Auth/OtwayRees.ML src/HOL/Auth/OtwayRees_AN.ML src/HOL/Auth/OtwayRees_Bad.ML

1997-05-05 paulson [Mon, 05 May 1997 12:15:20 +0200] rev 3101
Again "norm" DOES NOT normalize bodies of abstractions

Showterm (used for tracing) now follows variable instantiations (in order
to make up for the "norm" change)
src/Provers/blast.ML

1997-05-02 wenzelm [Fri, 02 May 1997 18:19:25 +0200] rev 3100
fixed comment;
doc-src/iman.sty