src/Pure/term.ML
Fri, 08 Dec 2023 14:48:17 +0100 wenzelm tuned -- eliminate clones;
Fri, 08 Dec 2023 13:09:39 +0100 wenzelm tuned;
Fri, 08 Dec 2023 12:05:56 +0100 wenzelm tuned;
Thu, 07 Dec 2023 15:25:29 +0100 wenzelm tuned;
Thu, 07 Dec 2023 12:12:13 +0100 wenzelm minor performance tuning: regular Same.operation;
Thu, 07 Dec 2023 11:48:34 +0100 wenzelm clarified signature: more standard argument order;
Thu, 07 Dec 2023 10:52:48 +0100 wenzelm tuned: more standard names;
Thu, 07 Dec 2023 10:40:59 +0100 wenzelm tuned: prefer Same.commit;
Thu, 07 Dec 2023 10:34:57 +0100 wenzelm tuned: more standard argument order;
Sat, 03 Sep 2022 17:37:46 +0200 wenzelm tuned signature;
Mon, 25 Oct 2021 17:37:24 +0200 wenzelm clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Mon, 04 Oct 2021 18:19:16 +0200 wenzelm tuned;
Sat, 02 Oct 2021 12:45:51 +0200 wenzelm clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;
Sat, 02 Oct 2021 11:56:11 +0200 wenzelm tuned, following Syntax_Trans.variant_abs;
Wed, 03 Mar 2021 16:54:21 +0100 wenzelm slightly more efficient Term.fastype_of (only little impact in regular applications);
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Fri, 23 Feb 2018 14:32:59 +0100 wenzelm tuned signature -- eliminated clones;
Fri, 05 Aug 2016 22:15:30 +0200 wenzelm more tight filtering;
Fri, 05 Aug 2016 16:36:03 +0200 wenzelm tuned whitespace;
Sun, 06 Mar 2016 16:19:02 +0100 wenzelm clarified treatment of fragments of Isabelle symbols during bootstrap;
Fri, 13 Nov 2015 14:11:54 +0100 wenzelm avoid vacuous quantification, as usual for shared variable scope;
Tue, 22 Sep 2015 16:17:49 +0200 wenzelm tuned signature;
Wed, 10 Jun 2015 21:49:02 +0200 wenzelm unused;
Tue, 09 Jun 2015 13:42:58 +0200 wenzelm clarified abstracted term bindings (again, see c8384ff11711);
Sat, 30 May 2015 19:28:51 +0200 wenzelm tuned whitespace;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Fri, 21 Mar 2014 12:34:50 +0100 wenzelm more qualified names;
Fri, 21 Mar 2014 11:42:32 +0100 wenzelm more qualified names;
Thu, 12 Dec 2013 22:56:28 +0100 wenzelm discontinued legacy_isub_isup;
Tue, 13 Aug 2013 17:26:22 +0200 wenzelm disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
Thu, 08 Aug 2013 17:36:14 +0200 wenzelm more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
Wed, 10 Jul 2013 16:25:26 +0200 wenzelm more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
Sun, 26 May 2013 21:05:03 +0200 wenzelm tuned;
Tue, 27 Nov 2012 19:22:36 +0100 wenzelm support for sub-structured identifier syntax (inactive);
Mon, 01 Oct 2012 16:37:22 +0200 wenzelm report sort assignment of visible type variables;
Sun, 15 Jul 2012 17:53:47 +0200 wenzelm prefer canonical fold_rev;
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
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;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 06 Jul 2011 20:14:13 +0200 wenzelm tuned errors;
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, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Wed, 01 Dec 2010 15:03:44 +0100 wenzelm more direct use of binder_types/body_type;
Wed, 01 Dec 2010 13:37:31 +0100 wenzelm tuned;
Wed, 01 Dec 2010 13:09:08 +0100 wenzelm just one Term.dest_funT;
Mon, 13 Sep 2010 00:10:29 +0200 wenzelm tuned;
Thu, 02 Sep 2010 00:48:07 +0200 wenzelm turned show_question_marks into proper configuration option;
Sat, 27 Mar 2010 15:47:57 +0100 wenzelm added Term.fold_atyps_sorts convenience;
Fri, 19 Feb 2010 11:06:22 +0100 haftmann added dest_comb
Thu, 28 Jan 2010 22:39:48 +0100 wenzelm tuned signature;
Sun, 15 Nov 2009 15:14:28 +0100 wenzelm tuned;
Mon, 09 Nov 2009 20:47:39 +0100 wenzelm locale_const/target_notation: uniform use of Term.aconv_untyped;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
less more (0) -100 -60 tip