1996-04-27 nipkow [Sat, 27 Apr 1996 12:05:58 +0200] rev 1693
Added R^1 = R
src/HOL/RelPow.ML

1996-04-26 paulson [Fri, 26 Apr 1996 13:33:51 +0200] rev 1692
Renaming of a lemma
src/ZF/ex/Comb.ML

1996-04-26 paulson [Fri, 26 Apr 1996 13:30:26 +0200] rev 1691
Fixed indenting
src/HOL/ex/Comb.ML

1996-04-26 clasohm [Fri, 26 Apr 1996 12:33:30 +0200] rev 1690
added changes by Konrad to prove_nchotomy
src/HOL/datatype.ML

1996-04-25 paulson [Thu, 25 Apr 1996 18:44:13 +0200] rev 1689
Fixed some unfortunate variable names
src/HOL/ex/Comb.ML

1996-04-25 paulson [Thu, 25 Apr 1996 17:31:07 +0200] rev 1688
Now contains HOLCF
doc-src/Isa-logics.eps

1996-04-25 oheimb [Thu, 25 Apr 1996 14:06:16 +0200] rev 1687
temporarily included settings for unification bounds again
src/HOL/MiniML/I.ML

1996-04-25 berghofe [Thu, 25 Apr 1996 13:03:57 +0200] rev 1686
Added functions mk_cntxt_splitthm and inst_split which instantiate
the split-rule before it is applied.
Inserted some comments.
src/Provers/splitter.ML

1996-04-25 paulson [Thu, 25 Apr 1996 12:49:44 +0200] rev 1685
Fixed a silly variable name
src/HOL/ex/Comb.thy

1996-04-25 paulson [Thu, 25 Apr 1996 12:45:14 +0200] rev 1684
Rearrangement and polishing to look for for publication
src/HOL/ex/Mutil.ML src/HOL/ex/Mutil.thy