| Mon, 08 Nov 2010 09:25:43 +0100 |
bulwahn |
adding code and theory for smallvalue generators, but do not setup the interpretation yet
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 13:16:43 +0200 |
blanchet |
integrated "smt" proof method with Sledgehammer
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:17:19 +0200 |
blanchet |
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 13:34:57 +0200 |
haftmann |
moved sledgehammer to Plain; tuned dependencies
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:41 +0200 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 19:31:00 +0100 |
blanchet |
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 15:06:38 +0100 |
blanchet |
reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 12:29:31 +0100 |
blanchet |
readded Predicate_Compile to Main
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 18:09:30 +0100 |
blanchet |
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:43:43 +0100 |
blanchet |
introduced Auto Nitpick in addition to Auto Quickcheck;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 14:51:47 +0200 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:32 +0200 |
haftmann |
moved Code_Index, Random and Quickcheck before Main
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 09:54:47 +0100 |
nipkow |
Moved Nat_Int_Bij into Library
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 13:43:19 +0100 |
blanchet |
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 00:21:59 +0100 |
wenzelm |
tuned header and description of boot files;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:14 +0200 |
wenzelm |
moved global ML bindings to global place;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 21:31:28 +0200 |
nipkow |
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:06:54 +0200 |
haftmann |
added dummy citiation
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:10 +0200 |
haftmann |
dropped theory PreList
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:53:58 +0100 |
haftmann |
consistent interacitve bootstrap of HOL-Main
|
file |
diff |
annotate
|
| Mon, 29 Oct 2007 16:13:41 +0100 |
wenzelm |
qualified Proofterm.proofs;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2007 17:55:28 +0200 |
paulson |
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Wed, 19 Sep 2007 12:17:13 +0200 |
berghofe |
Enclosed end_theory in text antiquotation to make LaTeX happy.
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 17:53:37 +0200 |
paulson |
metis now available in PreList
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:54 +0200 |
wenzelm |
HOL_proofs;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:26 +0200 |
haftmann |
minimal import
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 21:45:15 +0100 |
wenzelm |
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
|
file |
diff |
annotate
|
| Fri, 25 Aug 2006 18:44:59 +0200 |
paulson |
replaced skolem declarations by automatic skolemization of everything
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 18:40:56 +0200 |
paulson |
skolem declarations for built-in theorems
|
file |
diff |
annotate
|
| Wed, 10 May 2006 16:23:21 +0200 |
wenzelm |
revert accidental text change;
|
file |
diff |
annotate
|
| Tue, 09 May 2006 14:18:40 +0200 |
haftmann |
introduced characters for code generator; some improved code lemmas for some list functions
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 17:37:54 +0100 |
paulson |
the "skolem" attribute and better initialization of the clause database
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 15:45:54 +0100 |
paulson |
restoring the old status of subset_refl
|
file |
diff |
annotate
|
| 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").
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 15:50:44 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 16:01:45 +0200 |
webertj |
header (title/ID) added
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 15:45:12 +0200 |
webertj |
typo fixed: rufute -> refute
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:38 +0200 |
wenzelm |
removed Commutative_Ring hacks;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:21 +0200 |
wenzelm |
minor cleanup, moved stuff in its proper place;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:45:17 +0200 |
paulson |
moving Commutative_Ring to the correct theory
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:14:58 +0200 |
wenzelm |
hide the rather generic names used in theory Commutative_Ring;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:37 +0200 |
wenzelm |
imports Commutative_Ring;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 11:51:31 +0200 |
berghofe |
Auxiliary functions to be used in generated code are now defined using "attach".
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 13:56:34 +0200 |
berghofe |
Moved some code lemmas from Main to Nat.
|
file |
diff |
annotate
|
| Tue, 28 Jun 2005 15:27:45 +0200 |
paulson |
Constant "If" is now local
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 19:30:53 +0100 |
webertj |
refute_params: default value itself=1 added (for type classes)
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 10 Dec 2004 16:48:29 +0100 |
berghofe |
Moved code generator setup for product type to Product_Type.thy
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:16:10 +0100 |
paulson |
all theories must be related to Reconstruction
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Mon, 19 Jul 2004 18:15:46 +0200 |
berghofe |
Moved code generator setup for lists to List.thy
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 26 May 2004 17:43:52 +0200 |
webertj |
new default parameters for refute
|
file |
diff |
annotate
|
| Fri, 26 Mar 2004 19:58:43 +0100 |
webertj |
satsolver=dpll
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 22:37:33 +0100 |
webertj |
changed default values for refute
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|
| Mon, 22 Sep 2003 16:01:36 +0200 |
berghofe |
Improved efficiency of code generated for < predicate on natural numbers.
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 14:55:17 +0200 |
berghofe |
- Installed specific code generator for equality enforcing that
|
file |
diff |
annotate
|
| Tue, 27 May 2003 17:39:43 +0200 |
berghofe |
Added term_of function for product type.
|
file |
diff |
annotate
|
| Mon, 16 Dec 2002 13:43:11 +0100 |
berghofe |
Added mk_int and mk_list.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:42:30 +0200 |
berghofe |
Added theory for setting up program extraction.
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 18:26:52 +0200 |
wenzelm |
moved stuff to List.thy;
|
file |
diff |
annotate
|
| Fri, 19 Apr 2002 14:51:33 +0200 |
berghofe |
code generator: wfrec combinator is now implemented by ML function wf_rec.
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 14:55:28 +0100 |
berghofe |
Declared characteristic equations for < on nat for code generation.
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 15:18:57 +0100 |
berghofe |
Tuned code generator setup.
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:35:11 +0100 |
wenzelm |
moved String into Main;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:28:26 +0200 |
berghofe |
Added code generator setup.
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 14:52:10 +0200 |
paulson |
Hilbert_Choice is needed only in Main itself
|
file |
diff |
annotate
|
| Fri, 24 Nov 2000 16:49:27 +0100 |
nipkow |
hide many names from Datatype_Universe.
|
file |
diff |
annotate
|
| Fri, 03 Nov 2000 21:33:15 +0100 |
wenzelm |
provide case names for rev_induct, rev_cases;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:40:17 +0200 |
wenzelm |
tuned declarations;
|
file |
diff |
annotate
|
| Wed, 06 Sep 2000 16:54:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:47:46 +0200 |
wenzelm |
lemmas [recdef_cong] = map_cong;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:28:06 +0200 |
wenzelm |
lemmas [mono] = lists_mono;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 17:53:49 +0200 |
wenzelm |
Main now new-style theory; added Main.ML for compatibility;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 10:33:37 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2000 19:42:19 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
file |
diff |
annotate
|
| Mon, 02 Aug 1999 11:24:30 +0200 |
paulson |
the SVC link-up
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:35:42 +0200 |
paulson |
NatBin: binary arithmetic for the naturals
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:37:40 +0200 |
paulson |
new theory IntDiv.thy
|
file |
diff |
annotate
|
| Fri, 04 Jun 1999 19:57:31 +0200 |
wenzelm |
Calculation.thy: Setup transitivity rules for calculational proofs.
|
file |
diff |
annotate
|
| Tue, 05 Jan 1999 17:27:59 +0100 |
nipkow |
In Main: moved Bin to the left to preserve the solver in its simpset.
|
file |
diff |
annotate
|
| Wed, 09 Sep 1998 17:14:19 +0200 |
oheimb |
changed order of included theories
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:23:25 +0200 |
oheimb |
cleanup for Fun.thy:
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 18:05:03 +0200 |
wenzelm |
theory Main includes everything;
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 17:34:55 +0200 |
wenzelm |
stepping stones;
|
file |
diff |
annotate
|