src/HOL/Tools/Function/size.ML
Tue, 24 Jan 2012 16:00:51 +0100 berghofe Use lookup_size rather than Datatype.get_info in is_poly to avoid
Fri, 16 Dec 2011 21:23:21 +0100 wenzelm eliminated old-fashioned Global_Theory.add_thms(s);
Fri, 16 Dec 2011 10:38:38 +0100 wenzelm tuned signature;
Mon, 12 Dec 2011 23:05:21 +0100 wenzelm datatype dtyp with explicit sort information;
Fri, 02 Dec 2011 14:54:25 +0100 wenzelm more antiquotations;
Fri, 02 Dec 2011 13:51:36 +0100 wenzelm do not open ML structures;
Fri, 02 Dec 2011 13:38:24 +0100 wenzelm tuned signature;
Wed, 30 Nov 2011 23:30:08 +0100 wenzelm discontinued obsolete datatype "alt_names";
Tue, 31 May 2011 11:21:47 +0200 krauss more precise authorship, reflecting my own ignorance and hg annotate
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 30 Dec 2010 23:42:06 +0100 wenzelm do not open auxiliary ML structures;
Fri, 26 Nov 2010 21:31:46 +0100 wenzelm explicit use of unprefix;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
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;
Wed, 11 Aug 2010 14:31:43 +0200 haftmann moved instantiation target formally to class_target.ML
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, 12 Mar 2010 12:14:30 +0100 bulwahn refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Tue, 09 Feb 2010 11:47:47 +0100 haftmann hide fact names clashing with fact names from Group.thy
Mon, 08 Feb 2010 17:12:27 +0100 haftmann hide fact Nat.add_0_right; make add_0_right from Groups priority
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;
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
Wed, 21 Oct 2009 17:34:35 +0200 blanchet renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Mon, 28 Sep 2009 10:20:21 +0200 haftmann avoid compound fields in datatype info record
Sun, 27 Sep 2009 09:52:23 +0200 haftmann registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
less more (0) tip