src/Pure/proofterm.ML
Mon, 23 Mar 2015 19:43:03 +0100 wenzelm local fixes may depend on goal params;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 18 Jul 2013 13:12:54 +0200 wenzelm immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
Sun, 30 Jun 2013 11:37:34 +0200 wenzelm backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
Thu, 27 Jun 2013 23:17:26 +0200 wenzelm manage option "proofs" within theory context -- with minor overhead for primitive inferences;
Sun, 23 Jun 2013 16:47:45 +0200 wenzelm support for XML data representation of proof terms;
Fri, 12 Apr 2013 14:54:14 +0200 wenzelm tuned signature;
Wed, 13 Feb 2013 15:40:59 +0100 wenzelm discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;
Thu, 24 Jan 2013 21:18:30 +0100 wenzelm avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;
Mon, 07 Jan 2013 21:49:59 +0100 wenzelm no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;
Mon, 19 Nov 2012 20:23:47 +0100 wenzelm theorem status about oracles/futures is no longer printed by default;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Sat, 20 Aug 2011 20:00:55 +0200 wenzelm more direct balanced version Ord_List.unions;
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;
Sat, 20 Aug 2011 18:11:17 +0200 wenzelm tuned future priorities (again);
Sat, 20 Aug 2011 16:06:27 +0200 wenzelm clarified fulfill_norm_proof: no join_thms yet;
Sat, 20 Aug 2011 15:52:29 +0200 wenzelm added Future.joins convenience;
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;
Fri, 19 Aug 2011 18:01:23 +0200 wenzelm tuned;
Wed, 10 Aug 2011 19:45:57 +0200 wenzelm avoid OldTerm operations -- with subtle changes of semantics;
Wed, 10 Aug 2011 19:21:28 +0200 wenzelm avoid OldTerm operations -- with subtle changes of semantics;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Tue, 09 Aug 2011 22:30:33 +0200 wenzelm misc tuning and clarification;
Tue, 09 Aug 2011 21:48:36 +0200 wenzelm tuned whitespace;
Wed, 13 Jul 2011 21:44:15 +0200 wenzelm recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Thu, 03 Feb 2011 19:27:04 +0100 wenzelm tuned comments;
Thu, 03 Feb 2011 19:21:12 +0100 wenzelm clarified Proofterm.proofs_enabled;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Mon, 31 Jan 2011 21:54:49 +0100 wenzelm more direct Future.bulk, which potentially reduces overhead for Par_List;
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
less more (0) -100 -60 tip