| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
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 18:11:17 +0200 |
wenzelm |
tuned future priorities (again);
|
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
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:45:57 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 22:30:33 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 21:48:36 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 21:44:15 +0200 |
wenzelm |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 22:55:47 +0200 |
wenzelm |
tuned signature -- corresponding to Scala version;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:27:04 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:21:12 +0100 |
wenzelm |
clarified Proofterm.proofs_enabled;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 23:02:53 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 22:57:01 +0100 |
wenzelm |
support named tasks, for improved tracing;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2011 21:54:49 +0100 |
wenzelm |
more direct Future.bulk, which potentially reduces overhead for Par_List;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:39:35 +0200 |
wenzelm |
always unconstrain thm proofs;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 11:09:26 +0200 |
wenzelm |
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:30:57 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 11:01:16 +0200 |
berghofe |
- outer_constraints with original variable names, to ensure that argsP is consistent with args
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 20:15:59 +0200 |
wenzelm |
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 18:47:07 +0200 |
wenzelm |
raise Fail uniformly for proofterm errors, which appear to be rather low-level;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 18:22:10 +0200 |
wenzelm |
unconstrainT operations on proofs, according to krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 17:25:53 +0200 |
wenzelm |
added Proofterm.get_name variants according to krauss/schropp;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 16:24:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 16:03:09 +0200 |
wenzelm |
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 15:24:59 +0200 |
wenzelm |
back-patching of axclass proofs;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 19:50:50 +0200 |
wenzelm |
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:38:59 +0200 |
wenzelm |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
|
file |
diff |
annotate
|
| Tue, 04 May 2010 12:30:15 +0200 |
wenzelm |
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 11:02:50 +0200 |
wenzelm |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 19:04:46 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Sat, 15 Nov 2008 21:31:23 +0100 |
wenzelm |
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 15:48:51 +0200 |
wenzelm |
added conditional add_oracles, keep oracles_of_proof private;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:13 +0200 |
wenzelm |
added Promise constructor, which is similar to Oracle but may be replaced later;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:45 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 07:20:32 +0100 |
haftmann |
Type.lookup now curried
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:58:40 +0200 |
berghofe |
Added function rew_proof (for pre-normalizing proofs).
|
file |
diff |
annotate
|
| Fri, 08 Jun 2007 18:13:58 +0200 |
berghofe |
Adapted Proofterm.bicompose_proof to Larry's changes in
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 16:40:16 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:14:33 +0200 |
haftmann |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 12:12:46 +0200 |
wenzelm |
moved term subst functions to TermSubst;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:54 +0200 |
wenzelm |
replaced maxidx_of_proof by maxidx_proof;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:12:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2006 20:01:42 +0200 |
wenzelm |
fold_proof_terms: canonical arguments;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:51 +0200 |
wenzelm |
added map_proof_terms_option;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:49 +0200 |
wenzelm |
added generalize rule;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 11:17:44 +0200 |
berghofe |
Added alternative version of thms_of_proof that does not recursively
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:13 +0100 |
wenzelm |
remove (op =);
|
file |
diff |
annotate
|