| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:07:01 +0200 |
blanchet |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 15:18:46 +0200 |
blanchet |
updated Z3 docs
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 14:57:16 +0200 |
blanchet |
update the Vampire related parts of the documentation
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
document local HOATPs
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 09:33:01 +0200 |
blanchet |
updated Sledgehammer docs
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
updated Sledgehammer documentation
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
clarify fine soundness point
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
document "simple_higher" type encoding
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:31 +0200 |
blanchet |
document "sound" option
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:26 +0200 |
blanchet |
removed "full_types" option from documentation
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed removed option from documentation
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 08:58:23 +0200 |
blanchet |
documentation tweaks
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 08:52:35 +0200 |
blanchet |
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 22:03:58 +0200 |
blanchet |
minor: curly brackets, not square brackets
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 21:58:29 +0200 |
blanchet |
document metis better in Sledgehammer docs
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't mention "metisX" so much in the docs -- it will go away soon
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
temporarily document "metisX"
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
document new explicit apply
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
file |
diff |
annotate
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more concise output
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor fixes to Sledgehammer docs
|
file |
diff |
annotate
|