| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:20:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2013 17:35:12 +0200 |
wenzelm |
turned pattern unify flag into configuration option (global only);
|
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
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 16:12:05 +0200 |
wenzelm |
unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 20:56:08 +0200 |
wenzelm |
updated comment to 46b90bbc370d;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 15:22:21 +0200 |
wenzelm |
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
|
file |
diff |
annotate
|
| Sun, 15 Jul 2012 17:53:47 +0200 |
wenzelm |
prefer canonical fold_rev;
|
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, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 22:22:01 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 14:13:59 +0100 |
wenzelm |
removed obscure/outdated material;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 17:41:36 +0100 |
wenzelm |
discontinued unused Thm.compress (again);
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
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 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
|