| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 14:58:56 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
| Tue, 14 Oct 2008 16:01:36 +0200 |
wenzelm |
renamed AtpThread to AtpWrapper;
|
file |
diff |
annotate
|
| Fri, 03 Oct 2008 20:10:43 +0200 |
wenzelm |
updated to new AtpManager;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:24 +0200 |
berghofe |
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 17:54:56 +0200 |
ballarin |
Changed naming scheme for theorems generated by interpretations.
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:05 +0100 |
wenzelm |
replaced 'ML' by diagnostic 'ML_command';
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 18:10:23 +0100 |
paulson |
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 22:34:26 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 16:41:36 +0100 |
chaieb |
Fixed dependency on Dense_Linear_Order
|
file |
diff |
annotate
|
| Wed, 06 Feb 2008 08:34:32 +0100 |
haftmann |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
file |
diff |
annotate
|
| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:06 +0100 |
haftmann |
explicit import of theory Main
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 08:47:30 +0100 |
haftmann |
removed subclass edge ordered_ring < lordered_ring
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 17:38:45 +0200 |
paulson |
some more metis calls
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 16:09:36 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 15:05:34 +0200 |
paulson |
more metis proofs
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 09:59:21 +0200 |
paulson |
metis method: used theorems
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 16:54:03 +0200 |
paulson |
new proofs found
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 19:18:23 +0200 |
paulson |
tidied using sledgehammer
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:07:26 +0200 |
wenzelm |
tuned proofs -- avoid implicit prems;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 13:23:33 +0200 |
paulson |
integration of Metis prover
|
file |
diff |
annotate
|