| Fri, 26 Aug 2011 22:14:12 +0200 |
wenzelm |
tuned Session.edit_node: update_perspective based on last_exec_offset;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:27:58 +0200 |
wenzelm |
tuned signature -- iterate subsumes both fold and get_first;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:18:42 +0200 |
wenzelm |
further clarification of Document.updated, based on last_common and after_entry;
|
changeset |
files
|
| Fri, 26 Aug 2011 16:06:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:56:30 +0200 |
wenzelm |
improved Document.edit: more accurate update_start and no_execs;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:09:54 +0200 |
wenzelm |
refined document state assignment: observe perspective, more explicit assignment message;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
changeset |
files
|
| Thu, 25 Aug 2011 17:38:12 +0200 |
wenzelm |
maintain last_execs assignment on Scala side;
|
changeset |
files
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
changeset |
files
|
| Thu, 25 Aug 2011 13:24:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:20:05 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:19:40 +0200 |
wenzelm |
tuned syntax -- avoid ambiguities;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:00:53 +0200 |
wenzelm |
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
|
changeset |
files
|
| Wed, 24 Aug 2011 09:23:26 -0700 |
huffman |
delete commented-out dead code
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:07 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
changeset |
files
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
changeset |
files
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
changeset |
files
|
| Wed, 24 Aug 2011 17:30:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 15:25:39 +0200 |
blanchet |
make sure that all facts are passed to ATP from minimizer
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
specify timeout for "sledgehammer_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 24 Aug 2011 10:59:22 +0900 |
Cezary Kaliszyk |
Quotient Package: add mem_rsp, mem_prs, tune proofs.
|
changeset |
files
|
| Tue, 23 Aug 2011 15:46:53 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
changeset |
files
|
| Tue, 23 Aug 2011 07:12:05 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 18:15:33 -0700 |
huffman |
merged
|
changeset |
files
|