| Sat, 20 Dec 2014 19:12:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 18 Dec 2014 15:21:54 +0100 |
wenzelm |
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:39:20 +0100 |
wenzelm |
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 13:12:54 +0200 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
file |
diff |
annotate
|
| Wed, 17 Jul 2013 09:32:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:02:47 +0200 |
wenzelm |
added ML antiquotation @{theory_context};
|
file |
diff |
annotate
|
| Thu, 07 Mar 2013 15:02:55 +0100 |
wenzelm |
tuned signature -- prefer terminology of Scala and Axiom;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 13:25:49 +0100 |
wenzelm |
check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Thu, 30 Jun 2011 16:50:26 +0200 |
wenzelm |
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
|
file |
diff |
annotate
|