src/Pure/term.ML
2016-08-05 wenzelm 2016-08-05 more tight filtering;
2016-08-05 wenzelm 2016-08-05 tuned whitespace;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2015-11-13 wenzelm 2015-11-13 avoid vacuous quantification, as usual for shared variable scope;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-06-10 wenzelm 2015-06-10 unused;
2015-06-09 wenzelm 2015-06-09 clarified abstracted term bindings (again, see c8384ff11711);
2015-05-30 wenzelm 2015-05-30 tuned whitespace;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-12-12 wenzelm 2013-12-12 discontinued legacy_isub_isup;
2013-08-13 wenzelm 2013-08-13 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-08 wenzelm 2013-08-08 more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
2013-07-10 wenzelm 2013-07-10 more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
2013-05-26 wenzelm 2013-05-26 tuned;
2012-11-27 wenzelm 2012-11-27 support for sub-structured identifier syntax (inactive);
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-07-15 wenzelm 2012-07-15 prefer canonical fold_rev;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
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-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-07-06 wenzelm 2011-07-06 tuned errors; more direct Name.uu_ for dummy abstractions;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-12-01 wenzelm 2010-12-01 tuned;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-09-13 wenzelm 2010-09-13 tuned;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-03-27 wenzelm 2010-03-27 added Term.fold_atyps_sorts convenience;
2010-02-19 haftmann 2010-02-19 added dest_comb
2010-01-28 wenzelm 2010-01-28 tuned signature;
2009-11-15 wenzelm 2009-11-15 tuned;
2009-11-09 wenzelm 2009-11-09 locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-26 wenzelm 2009-07-26 lambda/cabs/all: named variants;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned;
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 close_schematic_term: uniform order of types/terms; tuned;
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;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-02-27 wenzelm 2009-02-27 tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
2009-02-13 kleing 2009-02-13 New command find_consts searching for constants by type (by Timothy Bourke).
2009-01-01 wenzelm 2009-01-01 added canonical add_const_names, add_consts;
2008-12-31 wenzelm 2008-12-31 updated header;
2008-12-31 wenzelm 2008-12-31 added declare_term_frees; tuned signature;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;