src/HOL/datatype.ML
Mon, 09 Feb 1998 18:09:35 +0100 nipkow Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
Fri, 09 Jan 1998 14:02:09 +0100 wenzelm eliminated make_ord;
Fri, 19 Dec 1997 10:27:23 +0100 wenzelm adapted to new sort function;
Fri, 07 Nov 1997 18:02:15 +0100 oheimb changed libraray function find to find_index_eq, currying it
Fri, 07 Nov 1997 08:25:02 +0100 nipkow Each datatype t now proves a theorem split_t_case_prem
Mon, 03 Nov 1997 21:15:08 +0100 wenzelm adapted to new datatypes thy info;
Thu, 30 Oct 1997 11:43:32 +0100 wenzelm PureThy.add_store_defs_i, PureThy.add_store_axioms;
Thu, 30 Oct 1997 09:45:03 +0100 nipkow For each datatype `t' there is now a theorem `split_t_case' of the form
Thu, 23 Oct 1997 12:48:48 +0200 wenzelm Sign.name_of;
Mon, 20 Oct 1997 11:14:55 +0200 wenzelm adapted to qualified names;
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 06 Oct 1997 19:13:29 +0200 wenzelm TODO: handle internal / external names;
Wed, 01 Oct 1997 18:13:41 +0200 wenzelm fully qualified names: Theory.add_XXX;
Wed, 06 Aug 1997 01:13:46 +0200 berghofe Moved some functions which used to be part of thy_data.ML
Wed, 23 Jul 1997 11:52:22 +0200 paulson Now Datatype.occs_in_prems prints the necessary warning ITSELF.
Tue, 22 Jul 1997 11:14:18 +0200 paulson Removal of the tactical STATE
Fri, 18 Jul 1997 13:55:09 +0200 wenzelm renamed |-> <-| <-> to Parse/PrintRule;
Fri, 23 May 1997 09:17:26 +0200 nipkow Added overloaded function `size' for all datatypes.
Thu, 22 May 1997 13:05:52 +0200 nipkow Added rotation to exhaust_tac.
Thu, 22 May 1997 09:20:28 +0200 nipkow Added exhaustion thm and exhaust_tac for each datatype.
Wed, 21 May 1997 10:09:21 +0200 nipkow Replaced Konrad's own add_term_names by the predefined one.
Thu, 15 May 1997 12:54:30 +0200 paulson Improved error message in "require_thy"
Tue, 06 May 1997 13:33:33 +0200 nipkow Stupid bug in induct_tac caused warning to always appear.
Mon, 05 May 1997 18:09:31 +0200 nipkow Cosmetic update of induct_tac; test first now.
Thu, 24 Apr 1997 18:06:46 +0200 nipkow Introduced a generic "induct_tac" which picks up the right induction scheme
Thu, 03 Apr 1997 09:46:42 +0200 nipkow Removed (Unit) in Prod.
Thu, 28 Nov 1996 12:31:33 +0100 paulson Replaced map...~~ by ListPair.map
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Fri, 02 Aug 1996 12:14:49 +0200 berghofe Replaced prove_case_cong by Konrad Slinds optimized version.
Tue, 18 Jun 1996 16:17:38 +0200 paulson Translation infixes <->, etc., no longer available at top-level
Fri, 26 Apr 1996 12:33:30 +0200 clasohm added changes by Konrad to prove_nchotomy
Fri, 19 Apr 1996 11:33:24 +0200 clasohm added Konrad's code for the datatype package
Wed, 13 Mar 1996 11:55:25 +0100 clasohm modified primrec so it can be used in MiniML/Type.thy
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Mon, 29 Jan 1996 13:48:37 +0100 clasohm changed the way simpsets and information about datatypes are stored
Tue, 21 Nov 1995 14:53:03 +0100 clasohm added call of store_datatype
Wed, 11 Oct 1995 11:22:35 +0100 nipkow All constants introduced by datatype now operate on class term explicitly.
Thu, 30 Mar 1995 13:07:59 +0200 clasohm removed unnecessary parentheses from the generated rules
Fri, 17 Mar 1995 22:46:26 +0100 clasohm fixed two severe bugs in calc_xrules and case_rule
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip