src/HOL/Tools/TFL/tfl.ML
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