| 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
|