src/HOL/Main.thy
Thu, 31 May 2007 18:16:54 +0200 wenzelm HOL_proofs;
Sun, 06 May 2007 21:49:26 +0200 haftmann minimal import
Wed, 08 Nov 2006 21:45:15 +0100 wenzelm incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
Fri, 25 Aug 2006 18:44:59 +0200 paulson replaced skolem declarations by automatic skolemization of everything
Tue, 08 Aug 2006 18:40:56 +0200 paulson skolem declarations for built-in theorems
Wed, 10 May 2006 16:23:21 +0200 wenzelm revert accidental text change;
Tue, 09 May 2006 14:18:40 +0200 haftmann introduced characters for code generator; some improved code lemmas for some list functions
Fri, 23 Dec 2005 17:37:54 +0100 paulson the "skolem" attribute and better initialization of the clause database
Thu, 01 Dec 2005 15:45:54 +0100 paulson restoring the old status of subset_refl
Wed, 19 Oct 2005 06:33:24 +0200 mengj Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
Thu, 29 Sep 2005 15:50:44 +0200 wenzelm explicit dependencies of SAT vs. Refute;
Fri, 23 Sep 2005 22:58:50 +0200 webertj new sat tactic imports resolution proofs from zChaff
Fri, 23 Sep 2005 16:01:45 +0200 webertj header (title/ID) added
Fri, 23 Sep 2005 15:45:12 +0200 webertj typo fixed: rufute -> refute
Tue, 20 Sep 2005 14:03:38 +0200 wenzelm removed Commutative_Ring hacks;
less more (0) -15 tip