| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:31:38 +0200 |
wenzelm |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 14:27:05 +0200 |
wenzelm |
added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 14:44:33 +0200 |
wenzelm |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 23:20:35 +0100 |
wenzelm |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 20:25:56 +0100 |
wenzelm |
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
dropped copy operation for legacy TheoryDataFun
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 00:11:26 +0100 |
wenzelm |
local mutex for theory content/identity operations;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:27:50 +0100 |
wenzelm |
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 22:46:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 21:26:45 +0200 |
wenzelm |
backpatching of structure Proof and ProofContext -- avoid odd aliases;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 14:43:35 +0100 |
wenzelm |
renamed structure ParList to Par_List;
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 14:33:49 +0100 |
wenzelm |
parallelized merge_data;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:35:18 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:06:24 +0100 |
wenzelm |
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 20:31:45 +0100 |
wenzelm |
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 00:08:07 +0100 |
wenzelm |
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
added reject_draft;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 16:03:44 +0200 |
wenzelm |
Thread.getLocal/setLocal;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:17 +0200 |
wenzelm |
added pprint_thy_ref;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 14:43:37 +0200 |
wenzelm |
names_of: exclude intermediate ids -- less verbosity;
|
file |
diff |
annotate
|