src/Pure/logic.ML
Tue, 01 Jun 2010 10:55:38 +0200 berghofe outer_constraints with original variable names, to ensure that argsP is consistent with args
Sun, 09 May 2010 19:15:21 +0200 wenzelm just one version of Thm.unconstrainT, which affects all variables;
Sun, 09 May 2010 18:09:30 +0200 wenzelm added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
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;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 22:48:24 +0200 wenzelm modernized Balanced_Tree;
Thu, 16 Jul 2009 22:58:07 +0200 wenzelm tuned incr_tvar_same;
Thu, 16 Jul 2009 21:29:02 +0200 wenzelm export incr_tvar_same;
Thu, 16 Jul 2009 21:00:09 +0200 wenzelm use structure Same;
Thu, 16 Jul 2009 00:24:11 +0200 wenzelm removed obsolete/unused legacy_varify;
Wed, 15 Jul 2009 21:42:24 +0200 wenzelm tuned comment;
Tue, 14 Jul 2009 12:18:52 +0200 wenzelm removed obsolete/unused legacy_unvarify;
Fri, 10 Jul 2009 00:47:17 +0200 wenzelm tuned varify/unvarify: use Term_Subst.map_XXX combinators;
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
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);
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Thu, 20 Nov 2008 00:03:47 +0100 wenzelm Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
Wed, 01 Oct 2008 14:17:06 +0200 wenzelm tuned comments;
Mon, 23 Jun 2008 23:45:47 +0200 wenzelm added all, is_all;
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
Mon, 21 Jan 2008 14:18:49 +0100 berghofe Removed Logic.auto_rename.
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Tue, 14 Aug 2007 13:20:16 +0200 wenzelm moved support for primitive defs to primitive_defs.ML;
Thu, 05 Jul 2007 20:01:34 +0200 wenzelm simplified has_meta_prems;
Tue, 19 Jun 2007 23:15:27 +0200 wenzelm balanced conjunctions;
Wed, 13 Jun 2007 00:02:00 +0200 wenzelm removed unused is_atomic;
Mon, 04 Jun 2007 21:04:19 +0200 wenzelm added is_atomic;
Wed, 09 May 2007 19:37:18 +0200 wenzelm removed unused mk_cond_defpair;
Wed, 29 Nov 2006 04:11:09 +0100 wenzelm simplified Logic.count_prems;
Fri, 24 Nov 2006 22:05:16 +0100 wenzelm added type_map;
Fri, 13 Oct 2006 18:08:48 +0200 berghofe Repaired strip_assums_hyp (now also works for goals not
Sat, 07 Oct 2006 01:31:11 +0200 wenzelm removed is_equals, is_implies;
Tue, 19 Sep 2006 23:15:39 +0200 wenzelm added name_classrel/arities/arity;
Fri, 15 Sep 2006 22:56:13 +0200 wenzelm renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
Tue, 11 Jul 2006 12:17:03 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Tue, 13 Jun 2006 23:41:47 +0200 wenzelm (un)varify: tuned exceptions;
Wed, 07 Jun 2006 02:01:28 +0200 wenzelm renamed Type.(un)varifyT to Logic.(un)varifyT;
Mon, 05 Jun 2006 21:54:21 +0200 wenzelm support embedded terms;
Thu, 13 Apr 2006 12:01:03 +0200 wenzelm added dest_conjunction_list;
Tue, 11 Apr 2006 16:00:02 +0200 wenzelm added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
Mon, 10 Apr 2006 00:33:49 +0200 wenzelm Term.itselfT;
Wed, 22 Feb 2006 22:18:39 +0100 wenzelm simplified Pure conjunction, based on actual const;
Sat, 18 Feb 2006 18:08:23 +0100 wenzelm dest_def: tuned error msg;
Thu, 16 Feb 2006 18:25:55 +0100 wenzelm dest_def: actually return beta-eta contracted equation;
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates;
Mon, 06 Feb 2006 20:59:05 +0100 wenzelm added generic dest_def (mostly from theory.ML);
Tue, 24 Jan 2006 00:43:23 +0100 wenzelm added dest_all;
Fri, 23 Dec 2005 15:16:48 +0100 wenzelm added mk_conjunction_list2;
Thu, 22 Dec 2005 00:28:58 +0100 wenzelm mk_conjunction: proper treatment of bounds;
Fri, 25 Nov 2005 18:58:34 +0100 wenzelm tuned;
Wed, 16 Nov 2005 17:45:27 +0100 wenzelm tuned;
Fri, 28 Oct 2005 22:27:57 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Thu, 18 Aug 2005 13:06:05 +0200 paulson optimization to incr_indexes?
Tue, 19 Jul 2005 17:21:51 +0200 wenzelm incr_tvar (from term.ML), incr_indexes: avoid garbage;
Fri, 15 Jul 2005 15:44:17 +0200 wenzelm tuned;
Thu, 14 Jul 2005 19:28:29 +0200 wenzelm occs no longer infix (structure not open);
Tue, 31 May 2005 11:53:21 +0200 wenzelm added nth_prem;
less more (0) -100 -60 tip