src/HOL/Tools/TFL/post.ML
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;
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Mon, 15 Mar 2010 20:27:23 +0100 wenzelm preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
Fri, 12 Mar 2010 12:14:30 +0100 bulwahn refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Thu, 25 Feb 2010 22:46:52 +0100 wenzelm modernized structure Split_Rule;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 21 Nov 2009 15:49:29 +0100 wenzelm explicitly mark some legacy freeze operations;
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;
Tue, 27 Oct 2009 22:56:14 +0100 wenzelm eliminated some old folds;
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Sat, 17 Oct 2009 01:05:59 +0200 wenzelm removed obsolete old goal command;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Fri, 27 Mar 2009 10:05:08 +0100 haftmann dropped legacy goal package call
Mon, 23 Mar 2009 19:01:16 +0100 haftmann moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
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, 10 Dec 2008 22:55:15 +0100 wenzelm more antiquotations;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Mon, 16 Jun 2008 17:54:43 +0200 wenzelm RuleInsts.read_instantiate;
Wed, 11 Jun 2008 18:02:00 +0200 wenzelm Drule.read_instantiate;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Sat, 29 Mar 2008 13:03:09 +0100 wenzelm eliminated quiete_mode ref (not really needed);
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Tue, 31 Jul 2007 00:56:26 +0200 wenzelm arith method setup: proper context;
Fri, 20 Jul 2007 14:28:05 +0200 haftmann dropped Nat.ML legacy bindings
Thu, 31 May 2007 13:18:52 +0200 wenzelm moved TFL files to canonical place;
less more (0) tip