| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 20:00:55 +0200 |
wenzelm |
more direct balanced version Ord_List.unions;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 19:21:03 +0200 |
wenzelm |
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 18:11:17 +0200 |
wenzelm |
tuned future priorities (again);
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 16:06:27 +0200 |
wenzelm |
clarified fulfill_norm_proof: no join_thms yet;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:52:29 +0200 |
wenzelm |
added Future.joins convenience;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 21:40:52 +0200 |
wenzelm |
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:45:57 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 22:30:33 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 21:48:36 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 21:44:15 +0200 |
wenzelm |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 22:55:47 +0200 |
wenzelm |
tuned signature -- corresponding to Scala version;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:27:04 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:21:12 +0100 |
wenzelm |
clarified Proofterm.proofs_enabled;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 23:02:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 21:54:49 +0100 |
wenzelm |
more direct Future.bulk, which potentially reduces overhead for Par_List;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:39:35 +0200 |
wenzelm |
always unconstrain thm proofs;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 11:09:26 +0200 |
wenzelm |
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:30:57 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:01:16 +0200 |
berghofe |
- outer_constraints with original variable names, to ensure that argsP is consistent with args
|
file |
diff |
annotate
|