1997-04-18 paulson [Fri, 18 Apr 1997 11:47:36 +0200] rev 2982
ex/LFilter is a new theory (and dependency)
src/HOL/IsaMakefile src/HOL/Makefile

1997-04-18 paulson [Fri, 18 Apr 1997 11:47:11 +0200] rev 2981
Automatic update
doc-src/ind-defs.bbl

1997-04-17 wenzelm [Thu, 17 Apr 1997 19:05:01 +0200] rev 2980
tuned error msgs;
src/Pure/type_infer.ML

1997-04-17 wenzelm [Thu, 17 Apr 1997 18:46:58 +0200] rev 2979
improved type check error messages;
src/Pure/sign.ML src/Pure/theory.ML src/Pure/thm.ML src/Pure/type.ML src/Pure/type_infer.ML

1997-04-17 wenzelm [Thu, 17 Apr 1997 18:45:43 +0200] rev 2978
renamed set_ap to setmp;
src/Pure/library.ML

1997-04-17 paulson [Thu, 17 Apr 1997 18:17:23 +0200] rev 2977
Automatic updates
doc-src/Intro/intro.bbl doc-src/Intro/intro.ind

1997-04-17 paulson [Thu, 17 Apr 1997 18:16:12 +0200] rev 2976
Removed the \date{} command in order to put the date of typesetting on the
title page
doc-src/Intro/intro.tex doc-src/Logics/logics.tex doc-src/Ref/ref.tex

1997-04-17 paulson [Thu, 17 Apr 1997 18:10:49 +0200] rev 2975
Corrected the informal description of coinductive definition
doc-src/Logics/HOL.tex doc-src/Logics/Old_HOL.tex

1997-04-17 paulson [Thu, 17 Apr 1997 18:10:12 +0200] rev 2974
Corrected the informal description of coinductive definition in sections 1
and 4.3, introducing the notion of "consistent with" a set of rules.

Final version for Milner Festschrift?
doc-src/ind-defs.tex

1997-04-17 nipkow [Thu, 17 Apr 1997 17:54:21 +0200] rev 2973
Added ability to have case expressions involving tuples. (via translation)
src/HOL/Prod.thy