| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 21:57:16 +0100 |
wenzelm |
generalized procs for rewrite_proof: allow skeleton;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 00:13:00 +0100 |
wenzelm |
revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 21:21:05 +0100 |
wenzelm |
fulfill_proof_future: tuned important special case of singleton promise;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 14:27:50 +0200 |
wenzelm |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 20:52:05 +0200 |
wenzelm |
fold_body_thms: pass pthm identifier;
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 21:08:13 +0200 |
wenzelm |
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 23:36:37 +0200 |
wenzelm |
get_name: cover only PThm, not PAxm;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 10:24:57 +0200 |
wenzelm |
prefer simultaneous join -- for improved scheduling;
|
file |
diff |
annotate
|
| Sun, 19 Jul 2009 17:08:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2009 22:53:02 +0200 |
wenzelm |
added join_bodies;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2009 00:33:57 +0200 |
wenzelm |
tuned prf_subst: use structure Same;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 22:58:45 +0200 |
wenzelm |
tuned incr_indexes;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 22:22:03 +0200 |
wenzelm |
tuned map_proof_terms_option;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 20:32:40 +0200 |
wenzelm |
use structure Same;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 19:58:52 +0200 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 20:55:44 +0200 |
wenzelm |
added pro-forma proof constructor Inclass;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2009 16:52:50 +0100 |
wenzelm |
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
|
file |
diff |
annotate
|