src/HOL/Tools/datatype_package.ML
Mon, 20 Aug 2007 18:07:30 +0200 haftmann using canonical instantiation interface
Fri, 10 Aug 2007 17:04:24 +0200 haftmann ClassPackage renamed to Class
Tue, 31 Jul 2007 21:19:20 +0200 wenzelm replaced dtK ref by datatype_distinctness_limit configuration option;
Thu, 17 May 2007 19:49:17 +0200 haftmann abstract size function in hologic.ML
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Tue, 24 Apr 2007 15:11:07 +0200 berghofe - Moved parse / print translations for case to datatype_case.ML
Sun, 15 Apr 2007 23:25:50 +0200 wenzelm removed obsolete TypeInfer.logicT -- use dummyT;
Sat, 14 Apr 2007 17:35:52 +0200 wenzelm cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Wed, 04 Apr 2007 23:29:38 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Tue, 20 Mar 2007 15:52:37 +0100 haftmann switched exception from arbitrary to undefined
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Mon, 11 Dec 2006 21:39:26 +0100 wenzelm advanced translation functions: Proof.context;
Thu, 07 Dec 2006 16:46:14 +0100 paulson Removal of theorem tagging, which the ATP linkup no longer requires,
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Wed, 22 Nov 2006 10:20:19 +0100 haftmann no explicit check for theory Nat
Sat, 18 Nov 2006 00:20:28 +0100 haftmann added instance for class size
Tue, 14 Nov 2006 00:15:38 +0100 wenzelm incorporated IsarThy into IsarCmd;
Wed, 08 Nov 2006 21:45:14 +0100 wenzelm case_tr': proper handling of authentic consts;
Wed, 08 Nov 2006 19:48:36 +0100 haftmann renamed DatatypeHooks.invoke to all
Wed, 08 Nov 2006 13:48:29 +0100 wenzelm removed theory NatArith (now part of Nat);
Sun, 05 Nov 2006 21:44:42 +0100 wenzelm case_tr: do not intern already internal consts;
Tue, 31 Oct 2006 14:58:16 +0100 haftmann cleaned up
Mon, 16 Oct 2006 14:07:21 +0200 haftmann slight cleanup
Sun, 01 Oct 2006 22:19:23 +0200 wenzelm removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
Tue, 26 Sep 2006 13:34:35 +0200 haftmann handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
Tue, 19 Sep 2006 15:22:05 +0200 haftmann code generation 2 adjustments
Thu, 03 Aug 2006 17:30:36 +0200 wenzelm RuleInsts.bires_inst_tac;
Wed, 26 Jul 2006 19:37:41 +0200 wenzelm Variable.import(T): result includes fixed types/terms;
Fri, 21 Jul 2006 14:47:22 +0200 haftmann hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
Fri, 21 Jul 2006 14:11:14 +0200 berghofe Some cases in "case ... of ..." expressions may now
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Sat, 08 Jul 2006 12:54:42 +0200 wenzelm distinct simproc/simpset: proper context;
Mon, 19 Jun 2006 20:21:30 +0200 wenzelm eliminated freeze/varify in favour of Variable.import/export/trade;
Tue, 13 Jun 2006 23:41:34 +0200 wenzelm ProjectRule now context dependent;
Sun, 11 Jun 2006 21:59:17 +0200 wenzelm avoid unqualified exception;
Wed, 24 May 2006 22:44:56 +0200 wenzelm add_datatype_axm: finalize specified consts;
Tue, 09 May 2006 10:09:37 +0200 haftmann added DatatypeHooks
Tue, 02 May 2006 20:42:35 +0200 wenzelm ThyInfo.the_theory;
Thu, 06 Apr 2006 16:10:46 +0200 haftmann cleanup in datatype package
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
Fri, 10 Feb 2006 09:09:07 +0100 haftmann improved code generator devarification
Fri, 10 Feb 2006 02:22:16 +0100 wenzelm Args/Attrib syntax: Context.generic;
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates;
Tue, 07 Feb 2006 08:47:43 +0100 haftmann slight improvements in code generation
Mon, 06 Feb 2006 11:01:28 +0100 haftmann subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
Tue, 31 Jan 2006 00:39:40 +0100 wenzelm advanced translations: Context.generic;
Fri, 27 Jan 2006 19:03:02 +0100 wenzelm moved theorem tags from Drule to PureThy;
Mon, 23 Jan 2006 11:37:53 +0100 paulson bugfix: induct_tac no longer raises THM "dest_state"
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Sun, 15 Jan 2006 19:58:53 +0100 wenzelm classical attributes: optional weight;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Tue, 10 Jan 2006 19:34:04 +0100 wenzelm generic attributes;
Mon, 09 Jan 2006 13:29:08 +0100 paulson _E suffix for compatibility with AddIffs
Thu, 29 Dec 2005 15:31:10 +0100 haftmann adaptions to changes in code generator
Thu, 22 Dec 2005 00:28:46 +0100 wenzelm *.inducts holds all projected rules;
Wed, 21 Dec 2005 17:00:57 +0100 haftmann slight improvements
less more (0) -100 -60 tip