| 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:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 20:52:05 +0200 |
wenzelm |
fold_body_thms: pass pthm identifier;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 12:09:55 +0200 |
wenzelm |
tuned internal source structure;
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 21:14:08 +0200 |
wenzelm |
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:53 +0200 |
wenzelm |
lambda/cabs/all: named variants;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 20:37:32 +0200 |
wenzelm |
simultaneous join_proofs;
|
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 18:42:05 +0200 |
wenzelm |
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
|
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, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 22:42:27 +0200 |
wenzelm |
clarified strip_shyps: proper type witnesses for present sorts;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 20:36:38 +0200 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
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 22:17:08 +0200 |
wenzelm |
strip_shyps: remove top sort, which is logically insignificant;
|
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:54:17 +0100 |
wenzelm |
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 22:56:17 +0100 |
wenzelm |
status_of: need to include local promises as well!
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 21:24:53 +0100 |
wenzelm |
display derivation status of thms;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 12:10:42 +0100 |
wenzelm |
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:52:30 +0100 |
wenzelm |
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:04:59 +0100 |
wenzelm |
moved Thm.def_name(_optional) to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 19:48:02 +0100 |
wenzelm |
Thm.add_oracle interface: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2009 00:42:12 +0100 |
wenzelm |
thm_proof: replaced lazy by composed futures;
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 21:47:02 +0100 |
wenzelm |
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
|
file |
diff |
annotate
|
| Sat, 10 Jan 2009 16:54:55 +0100 |
wenzelm |
added pending_groups -- accumulates task groups of local derivations only;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
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
|
| Sat, 06 Dec 2008 00:09:01 +0100 |
wenzelm |
renamed force_proof to join_proof;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 20:38:40 +0100 |
wenzelm |
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:05:14 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 00:23:37 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:02:56 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Sun, 23 Nov 2008 17:25:56 +0100 |
wenzelm |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 22:25:36 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:25 +0100 |
wenzelm |
refined notion of derivation, consiting of promises and proof_body;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:05 +0200 |
wenzelm |
renamed get_axiom_i to axiom, removed obsolete get_axiom;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 16:53:10 +0200 |
wenzelm |
join results in isolation;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:33 +0200 |
wenzelm |
added weaken_sorts;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:18:18 +0200 |
wenzelm |
renamed promise to future, tuned related interfaces;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:00 +0200 |
wenzelm |
more precise join_futures, improved termination;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 22:02:44 +0200 |
wenzelm |
export explicit joint_futures, removed Theory.at_end hook;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:19 +0200 |
wenzelm |
simplified promise;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:35:02 +0200 |
wenzelm |
abtract types: plain datatype with opaque signature matching;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
file |
diff |
annotate
|