isabelle: Changelog

obua [Tue, 29 Jun 2004 10:07:56 +0200] rev 15009

support for sparse matrices

paulson [Mon, 28 Jun 2004 11:15:13 +0200] rev 15008

new method for explicit classical resolution

paulson [Fri, 25 Jun 2004 15:03:05 +0200] rev 15007

auto update

skalberg [Fri, 25 Jun 2004 14:30:55 +0200] rev 15006

Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.

paulson [Thu, 24 Jun 2004 17:54:53 +0200] rev 15005

Norbert Voelker

paulson [Thu, 24 Jun 2004 17:52:55 +0200] rev 15004

ringpower to recpower

paulson [Thu, 24 Jun 2004 17:52:02 +0200] rev 15003

replaced monomorphic abs definitions by abs_if

paulson [Thu, 24 Jun 2004 17:51:28 +0200] rev 15002

tidied

skalberg [Wed, 23 Jun 2004 14:44:22 +0200] rev 15001

Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.

wenzelm [Wed, 23 Jun 2004 09:09:18 +0200] rev 15000

tuned;

isabelle