src/Pure/thm.ML
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Wed, 29 May 2013 16:12:05 +0200 wenzelm unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Wed, 03 Apr 2013 20:56:08 +0200 wenzelm updated comment to 46b90bbc370d;
Fri, 30 Nov 2012 22:38:06 +0100 wenzelm print formal entities with markup;
Mon, 19 Nov 2012 20:23:47 +0100 wenzelm theorem status about oracles/futures is no longer printed by default;
Thu, 30 Aug 2012 15:22:21 +0200 wenzelm proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
Sun, 15 Jul 2012 17:53:47 +0200 wenzelm prefer canonical fold_rev;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Tue, 14 Feb 2012 22:22:01 +0100 wenzelm tuned signature;
Wed, 25 Jan 2012 14:13:59 +0100 wenzelm removed obscure/outdated material;
Sat, 14 Jan 2012 20:05:58 +0100 wenzelm renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
Thu, 10 Nov 2011 17:41:36 +0100 wenzelm discontinued unused Thm.compress (again);
Thu, 03 Nov 2011 22:51:37 +0100 wenzelm tuned signature;
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 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;
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
Tue, 09 Aug 2011 23:54:17 +0200 berghofe rename_bvs now avoids introducing name clashes between schematic variables
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;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Wed, 20 Apr 2011 13:54:07 +0200 wenzelm added Theory.nodes_of convenience;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Thu, 03 Feb 2011 20:13:49 +0100 wenzelm thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
Thu, 03 Feb 2011 19:27:04 +0100 wenzelm tuned comments;
Thu, 28 Oct 2010 22:23:11 +0200 wenzelm type attribute is derived concept outside the kernel;
Mon, 25 Oct 2010 11:22:30 +0200 wenzelm recovered some odd two-dimensional layout;
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Wed, 25 Aug 2010 15:12:49 +0200 wenzelm structure Thm: less pervasive names;
Thu, 03 Jun 2010 23:17:57 +0200 wenzelm eliminated ML structure alias;
Wed, 02 Jun 2010 21:39:35 +0200 wenzelm always unconstrain thm proofs;
Wed, 19 May 2010 10:17:05 +0200 haftmann dropped legacy_unconstrainT
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;
Sun, 09 May 2010 22:06:24 +0200 wenzelm reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
Sun, 09 May 2010 19:50:56 +0200 wenzelm Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
Sun, 09 May 2010 19:15:21 +0200 wenzelm just one version of Thm.unconstrainT, which affects all variables;
Sat, 08 May 2010 16:53:53 +0200 wenzelm renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
Sat, 08 May 2010 16:24:44 +0200 wenzelm tuned signature;
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 11:02:50 +0200 wenzelm renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
Mon, 03 May 2010 20:13:36 +0200 wenzelm renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
Mon, 03 May 2010 16:26:47 +0200 wenzelm minor tuning of Thm.strip_shyps -- no longer pervasive;
Mon, 03 May 2010 15:34:55 +0200 wenzelm simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
Sun, 25 Apr 2010 23:09:32 +0200 wenzelm renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
Sat, 27 Mar 2010 15:47:57 +0100 wenzelm added Term.fold_atyps_sorts convenience;
Sun, 21 Mar 2010 22:13:31 +0100 wenzelm Logic.mk_of_sort convenience;
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
Sat, 21 Nov 2009 15:49:29 +0100 wenzelm explicitly mark some legacy freeze operations;
Mon, 16 Nov 2009 21:57:16 +0100 wenzelm generalized procs for rewrite_proof: allow skeleton;
less more (0) -300 -100 -60 tip