src/Pure/proofterm.ML
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Wed, 01 Sep 2010 15:33:59 +0200 haftmann replaced Table.map' by Table.map
Wed, 02 Jun 2010 21:39:35 +0200 wenzelm always unconstrain thm proofs;
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);
Tue, 01 Jun 2010 11:30:57 +0200 berghofe merged
Tue, 01 Jun 2010 11:01:16 +0200 berghofe - outer_constraints with original variable names, to ensure that argsP is consistent with args
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
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;
Thu, 13 May 2010 21:36:38 +0200 wenzelm conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
Thu, 13 May 2010 20:15:59 +0200 wenzelm avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
Thu, 13 May 2010 18:47:07 +0200 wenzelm raise Fail uniformly for proofterm errors, which appear to be rather low-level;
Thu, 13 May 2010 18:22:10 +0200 wenzelm unconstrainT operations on proofs, according to krauss/schropp;
Thu, 13 May 2010 17:25:53 +0200 wenzelm added Proofterm.get_name variants according to krauss/schropp;
Sat, 08 May 2010 16:24:44 +0200 wenzelm tuned signature;
Sat, 08 May 2010 16:03:09 +0200 wenzelm added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
Sat, 08 May 2010 15:24:59 +0200 wenzelm back-patching of axclass proofs;
Fri, 07 May 2010 19:50:50 +0200 wenzelm strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
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:
Tue, 04 May 2010 12:30:15 +0200 wenzelm simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
Tue, 04 May 2010 11:02:50 +0200 wenzelm renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
Sun, 21 Mar 2010 19:04:46 +0100 wenzelm do not open ML structures;
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;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Mon, 16 Nov 2009 21:57:16 +0100 wenzelm generalized procs for rewrite_proof: allow skeleton;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 05 Nov 2009 00:13:00 +0100 wenzelm revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
Wed, 04 Nov 2009 21:21:05 +0100 wenzelm fulfill_proof_future: tuned important special case of singleton promise;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
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;
Wed, 30 Sep 2009 22:24:57 +0200 wenzelm eliminated redundant parameters;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Mon, 28 Sep 2009 20:52:05 +0200 wenzelm fold_body_thms: pass pthm identifier;
Sun, 27 Sep 2009 21:08:13 +0200 wenzelm fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
Fri, 24 Jul 2009 23:36:37 +0200 wenzelm get_name: cover only PThm, not PAxm;
Tue, 21 Jul 2009 10:24:57 +0200 wenzelm prefer simultaneous join -- for improved scheduling;
Sun, 19 Jul 2009 17:08:34 +0200 wenzelm tuned;
Sat, 18 Jul 2009 22:53:02 +0200 wenzelm added join_bodies;
Sat, 18 Jul 2009 00:33:57 +0200 wenzelm tuned prf_subst: use structure Same;
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Thu, 16 Jul 2009 22:58:45 +0200 wenzelm tuned incr_indexes;
Thu, 16 Jul 2009 22:22:03 +0200 wenzelm tuned map_proof_terms_option;
Thu, 16 Jul 2009 20:32:40 +0200 wenzelm use structure Same;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
Thu, 02 Jul 2009 20:55:44 +0200 wenzelm added pro-forma proof constructor Inclass;
Wed, 25 Mar 2009 16:52:50 +0100 wenzelm removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
Tue, 24 Mar 2009 22:55:49 +0100 wenzelm status_of: simultaneous list;
Tue, 24 Mar 2009 21:24:53 +0100 wenzelm display derivation status of thms;
Fri, 27 Feb 2009 16:38:52 +0100 wenzelm eliminated NJ's List.nth;
Tue, 27 Jan 2009 14:28:51 +0100 wenzelm thm_proof: recovered single-threaded version;
Tue, 27 Jan 2009 00:42:12 +0100 wenzelm thm_proof: replaced lazy by composed futures;
Tue, 27 Jan 2009 00:29:37 +0100 wenzelm proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
less more (0) -100 -60 tip