| 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
|
| Tue, 24 Mar 2009 22:55:49 +0100 |
wenzelm |
status_of: simultaneous list;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 21:24:53 +0100 |
wenzelm |
display derivation status of thms;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:38:52 +0100 |
wenzelm |
eliminated NJ's List.nth;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2009 14:28:51 +0100 |
wenzelm |
thm_proof: recovered single-threaded version;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2009 00:42:12 +0100 |
wenzelm |
thm_proof: replaced lazy by composed futures;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2009 00:29:37 +0100 |
wenzelm |
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 21:49:09 +0100 |
wenzelm |
freeze_thaw: canonical Term.add_XXX operations;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:00:21 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
file |
diff |
annotate
|
| Sun, 23 Nov 2008 18:37:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 23 Nov 2008 17:27:15 +0100 |
wenzelm |
eliminated finish_proof, keep pre/post normalization of results separate;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 22:25:30 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 23:34:35 +0100 |
wenzelm |
finish_proof: undefined promises may occur here;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 23:17:11 +0100 |
wenzelm |
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 22:12:41 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 18:18:45 +0100 |
berghofe |
Frees in PThms are now quantified in the order of their appearance in the
|
file |
diff |
annotate
|