isabelle: Changelog

paulson [Fri, 13 Dec 2002 13:47:13 +0100] rev 13748

deleted redundant line

paulson [Thu, 12 Dec 2002 11:38:18 +0100] rev 13747

Better treatment of equality in premises of inductive definitions. Less backtracking.

ballarin [Thu, 12 Dec 2002 11:33:48 +0100] rev 13746

Fixed error that affected document preperation.

ballarin [Wed, 11 Dec 2002 10:12:48 +0100] rev 13745

HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.

berghofe [Tue, 10 Dec 2002 10:40:32 +0100] rev 13744

Added size_of_proof.

ballarin [Mon, 09 Dec 2002 10:38:56 +0100] rev 13743

Fixed bug in simpdata.ML that prevented the use of congruence rules from a locale. (mk_meta_cong did wrongly convert metahyps to hyps)

oheimb [Fri, 06 Dec 2002 15:16:30 +0100] rev 13742

corrected swallowing of newlines after end-of-ignore

nipkow [Fri, 06 Dec 2002 11:09:02 +0100] rev 13741

*** empty log message ***

Thu, 05 Dec 2002 18:44:16 +0100 for dvi target

kleing [Thu, 05 Dec 2002 18:44:16 +0100] rev 13740

for dvi target

kleing [Thu, 05 Dec 2002 17:12:07 +0100] rev 13739

exercise collection

isabelle