src/ZF/Tools/inductive_package.ML
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Sat, 30 Dec 2006 16:08:00 +0100 wenzelm removed conditional combinator;
Tue, 14 Nov 2006 00:15:38 +0100 wenzelm incorporated IsarThy into IsarCmd;
Sat, 05 Aug 2006 14:52:57 +0200 wenzelm tuned;
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Tue, 10 Jan 2006 19:34:04 +0100 wenzelm generic attributes;
Fri, 16 Dec 2005 09:00:11 +0100 haftmann re-arranged tuples (theory * 'a) to ('a * theory) in Pure
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Wed, 19 Oct 2005 21:52:50 +0200 wenzelm removed add_inductive_x;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
Thu, 08 Sep 2005 16:09:23 +0200 haftmann introduces some modern-style AList operations
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Thu, 14 Jul 2005 19:28:40 +0200 wenzelm no open Logic;
Fri, 17 Jun 2005 18:33:42 +0200 wenzelm Context.names_of;
Wed, 13 Apr 2005 18:45:25 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:12:22 +0100 berghofe Replaced xstring by thmref.
Thu, 12 Dec 2002 11:38:18 +0100 paulson Better treatment of equality in premises of inductive definitions. Less
Fri, 04 Oct 2002 15:23:58 +0200 paulson Fixed bug involving inductive definitions with equalities in the premises.
Wed, 20 Feb 2002 00:53:53 +0100 wenzelm Symbol.bump_string;
Tue, 12 Feb 2002 20:28:27 +0100 wenzelm got rid of explicit marginal comments (now stripped earlier from input);
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 11 Jan 2002 14:53:30 +0100 wenzelm replace gen_all by forall_elim_vars_safe;
Mon, 19 Nov 2001 20:47:57 +0100 wenzelm tuned;
Fri, 16 Nov 2001 22:09:44 +0100 wenzelm actually store "coinduct" rule;
Wed, 14 Nov 2001 23:20:41 +0100 wenzelm case_names;
Wed, 14 Nov 2001 18:46:30 +0100 wenzelm adapted primrec/datatype to Isar;
Tue, 13 Nov 2001 22:20:51 +0100 wenzelm rearranged inductive package for Isar;
Fri, 09 Nov 2001 22:53:41 +0100 wenzelm support co/inductive definitions in new-style theories;
Thu, 04 Oct 2001 15:29:37 +0200 wenzelm qualify MetaSimplifier;
Thu, 13 Jul 2000 23:20:57 +0200 wenzelm adapted PureThy.add_defs_i;
Fri, 05 May 2000 22:37:04 +0200 wenzelm use Sign.simple_read_term;
Mon, 13 Mar 2000 13:28:31 +0100 wenzelm adapted to new PureThy.add_thms etc.;
Mon, 04 Oct 1999 21:39:10 +0200 wenzelm mk_frees, assume_read moved here;
Tue, 21 Sep 1999 19:11:07 +0200 nipkow Mod because of new solver interface.
Wed, 03 Feb 1999 13:29:24 +0100 paulson standard spelling: type-checking
Tue, 19 Jan 1999 11:18:11 +0100 paulson removal of the (thm list) argument of mk_cases
Tue, 12 Jan 1999 15:17:37 +0100 wenzelm eliminated global/local names;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Mon, 28 Dec 1998 16:58:00 +0100 paulson revised inductive definition package
less more (0) tip