isabelle: Changelog

paulson [Mon, 28 Aug 2006 18:15:32 +0200] rev 20421

tidied

webertj [Mon, 28 Aug 2006 16:10:44 +0200] rev 20420

encode clauses as Isar premises, rather than as object-logic &, for faster parsing

paulson [Fri, 25 Aug 2006 18:48:58 +0200] rev 20419

abstraction of lambda-expressions

paulson [Fri, 25 Aug 2006 18:48:09 +0200] rev 20418

tidied

paulson [Fri, 25 Aug 2006 18:47:36 +0200] rev 20417

better skolemization, using first-order resolution rather than hoping for the right result

paulson [Fri, 25 Aug 2006 18:46:24 +0200] rev 20416

using inc

paulson [Fri, 25 Aug 2006 18:45:57 +0200] rev 20415

explicit type variables prevent empty sorts

paulson [Fri, 25 Aug 2006 18:44:59 +0200] rev 20414

replaced skolem declarations by automatic skolemization of everything

webertj [Fri, 25 Aug 2006 00:10:10 +0200] rev 20413

avoid duplicate tactics

webertj [Thu, 24 Aug 2006 23:51:46 +0200] rev 20412

additional list of tactics that can be added to arith

isabelle