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;
Sat, 17 Sep 2005 18:11:21 +0200 wenzelm minor cleanup, moved stuff in its proper place;
Thu, 15 Sep 2005 17:45:17 +0200 paulson moving Commutative_Ring to the correct theory
Wed, 14 Sep 2005 23:14:58 +0200 wenzelm hide the rather generic names used in theory Commutative_Ring;
Wed, 14 Sep 2005 22:04:37 +0200 wenzelm imports Commutative_Ring;
Tue, 12 Jul 2005 11:51:31 +0200 berghofe Auxiliary functions to be used in generated code are now defined using "attach".
Fri, 01 Jul 2005 13:56:34 +0200 berghofe Moved some code lemmas from Main to Nat.
Tue, 28 Jun 2005 15:27:45 +0200 paulson Constant "If" is now local
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
Thu, 28 Apr 2005 17:56:58 +0200 paulson fixed treatment of higher-order simprules
Mon, 07 Mar 2005 19:30:53 +0100 webertj refute_params: default value itself=1 added (for type classes)
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Fri, 10 Dec 2004 16:48:29 +0100 berghofe Moved code generator setup for product type to Product_Type.thy
Tue, 07 Dec 2004 16:16:10 +0100 paulson all theories must be related to Reconstruction
Fri, 20 Aug 2004 12:21:03 +0200 paulson proof reconstruction for external ATPs
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Mon, 19 Jul 2004 18:15:46 +0200 berghofe Moved code generator setup for lists to List.thy
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 26 May 2004 17:43:52 +0200 webertj new default parameters for refute
Fri, 26 Mar 2004 19:58:43 +0100 webertj satsolver=dpll
Wed, 10 Mar 2004 22:37:33 +0100 webertj changed default values for refute
Mon, 08 Mar 2004 11:12:06 +0100 paulson generic theorems about exponentials; general tidying up
Sat, 10 Jan 2004 13:35:10 +0100 webertj Adding 'refute' to HOL.
Mon, 22 Sep 2003 16:01:36 +0200 berghofe Improved efficiency of code generated for < predicate on natural numbers.
Fri, 11 Jul 2003 14:55:17 +0200 berghofe - Installed specific code generator for equality enforcing that
Tue, 27 May 2003 17:39:43 +0200 berghofe Added term_of function for product type.
Mon, 16 Dec 2002 13:43:11 +0100 berghofe Added mk_int and mk_list.
Sun, 21 Jul 2002 15:42:30 +0200 berghofe Added theory for setting up program extraction.
Tue, 16 Jul 2002 18:26:52 +0200 wenzelm moved stuff to List.thy;
Fri, 19 Apr 2002 14:51:33 +0200 berghofe code generator: wfrec combinator is now implemented by ML function wf_rec.
Thu, 20 Dec 2001 14:55:28 +0100 berghofe Declared characteristic equations for < on nat for code generation.
Mon, 10 Dec 2001 15:18:57 +0100 berghofe Tuned code generator setup.
Sat, 03 Nov 2001 01:35:11 +0100 wenzelm moved String into Main;
Fri, 31 Aug 2001 16:28:26 +0200 berghofe Added code generator setup.
Wed, 08 Aug 2001 14:52:10 +0200 paulson Hilbert_Choice is needed only in Main itself
Fri, 24 Nov 2000 16:49:27 +0100 nipkow hide many names from Datatype_Universe.
Fri, 03 Nov 2000 21:33:15 +0100 wenzelm provide case names for rev_induct, rev_cases;
Wed, 18 Oct 2000 23:40:17 +0200 wenzelm tuned declarations;
Wed, 06 Sep 2000 16:54:12 +0200 wenzelm tuned;
Tue, 05 Sep 2000 18:47:46 +0200 wenzelm lemmas [recdef_cong] = map_cong;
Fri, 01 Sep 2000 00:28:06 +0200 wenzelm lemmas [mono] = lists_mono;
Fri, 18 Aug 2000 17:53:49 +0200 wenzelm Main now new-style theory; added Main.ML for compatibility;
Thu, 17 Aug 2000 10:33:37 +0200 wenzelm fixed deps;
Wed, 26 Jul 2000 19:42:19 +0200 nipkow *** empty log message ***
Thu, 16 Mar 2000 00:35:27 +0100 wenzelm added HOL/PreLIst.thy;
less more (0) -60 tip