src/Pure/logic.ML
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-11-05 wenzelm 2011-11-05 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;
2011-11-03 wenzelm 2011-11-03 tuned signature;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2010-06-01 berghofe 2010-06-01 outer_constraints with original variable names, to ensure that argsP is consistent with args
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 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);
2010-03-21 wenzelm 2010-03-21 Logic.mk_of_sort convenience;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-07-16 wenzelm 2009-07-16 tuned incr_tvar_same; export tuned version of incr_indexes_same;
2009-07-16 wenzelm 2009-07-16 export incr_tvar_same; tuned;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned;
2009-07-16 wenzelm 2009-07-16 removed obsolete/unused legacy_varify;
2009-07-15 wenzelm 2009-07-15 tuned comment;
2009-07-14 wenzelm 2009-07-14 removed obsolete/unused legacy_unvarify;
2009-07-10 wenzelm 2009-07-10 tuned varify/unvarify: use Term_Subst.map_XXX combinators;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-03-16 wenzelm 2009-03-16 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);
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-01 wenzelm 2008-10-01 tuned comments;
2008-06-23 wenzelm 2008-06-23 added all, is_all; improved dest_all; added implies (from term.ML);
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-01-21 berghofe 2008-01-21 Removed Logic.auto_rename.
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-08-14 wenzelm 2007-08-14 moved support for primitive defs to primitive_defs.ML;
2007-07-05 wenzelm 2007-07-05 simplified has_meta_prems;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-13 wenzelm 2007-06-13 removed unused is_atomic;
2007-06-04 wenzelm 2007-06-04 added is_atomic; removed unused is_all;
2007-05-09 wenzelm 2007-05-09 removed unused mk_cond_defpair;
2006-11-29 wenzelm 2006-11-29 simplified Logic.count_prems;
2006-11-24 wenzelm 2006-11-24 added type_map;
2006-10-13 berghofe 2006-10-13 Repaired strip_assums_hyp (now also works for goals not in hhf normal form).
2006-10-07 wenzelm 2006-10-07 removed is_equals, is_implies; tuned;
2006-09-19 wenzelm 2006-09-19 added name_classrel/arities/arity;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.invent_list;
2006-06-13 wenzelm 2006-06-13 (un)varify: tuned exceptions;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-04-13 wenzelm 2006-04-13 added dest_conjunction_list; close_form: canonical order of variables;
2006-04-11 wenzelm 2006-04-11 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction, based on actual const;
2006-02-18 wenzelm 2006-02-18 dest_def: tuned error msg;
2006-02-16 wenzelm 2006-02-16 dest_def: actually return beta-eta contracted equation;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);
2006-01-24 wenzelm 2006-01-24 added dest_all;
2005-12-23 wenzelm 2005-12-23 added mk_conjunction_list2;
2005-12-22 wenzelm 2005-12-22 mk_conjunction: proper treatment of bounds; added dest_conjunction(s);
2005-11-25 wenzelm 2005-11-25 tuned;