src/HOL/Tools/TFL/tfl.ML
Mon, 01 Sep 2014 16:17:46 +0200 blanchet tuned structure inclusion
Mon, 18 Aug 2014 17:19:58 +0200 blanchet reordered some (co)datatype property names for more consistency
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sat, 01 Feb 2014 18:42:46 +0100 wenzelm proper context for printing;
Sun, 12 Jan 2014 16:42:02 +0100 wenzelm clarified context;
Wed, 01 Jan 2014 14:29:22 +0100 wenzelm clarified simplifier context;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString;
Wed, 15 Dec 2010 15:11:56 +0100 wenzelm avoid ML structure aliases (especially single-letter abbreviations);
Wed, 03 Nov 2010 10:48:55 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Mon, 06 Sep 2010 19:11:01 +0200 wenzelm ML_Context.thm;
Thu, 19 Aug 2010 16:03:01 +0200 haftmann corrected some long-overseen misperceptions in recdef
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Mon, 03 May 2010 20:53:49 +0200 wenzelm replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
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 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Mon, 15 Mar 2010 20:27:23 +0100 wenzelm preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
Tue, 09 Mar 2010 14:18:06 +0100 wenzelm renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Wed, 21 Oct 2009 12:08:52 +0200 haftmann merged
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 10:15:31 +0200 haftmann removed old-style \ and \\ infixes
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 28 Aug 2009 21:04:03 +0200 wenzelm modernized messages -- eliminated ctyp/cterm operations;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
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;
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Thu, 28 Feb 2008 12:56:33 +0100 wenzelm removed legacy ML bindings;
Thu, 30 Aug 2007 22:35:34 +0200 wenzelm replaced ProofContext.infer_types by general Syntax.check_terms;
Thu, 31 May 2007 13:18:52 +0200 wenzelm moved TFL files to canonical place;
less more (0) tip