src/HOL/Tools/primrec_package.ML
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Fri, 20 Oct 2006 10:44:47 +0200 haftmann fold cleanup
Fri, 13 Oct 2006 18:23:37 +0200 berghofe Moved old inductive package to old_inductive_package.ML
Mon, 02 Oct 2006 23:01:00 +0200 haftmann added gen_primrec
Fri, 21 Jul 2006 14:46:27 +0200 haftmann exported equation transformator
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Sat, 20 May 2006 23:36:57 +0200 wenzelm added syntax for 'unchecked';
Sat, 13 May 2006 02:51:49 +0200 wenzelm added add_primrec_unchecked_i;
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates;
Mon, 06 Feb 2006 11:01:28 +0100 haftmann subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 17:26:26 +0100 haftmann removed thms 'swap' and 'nth_map' from ML toplevel
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;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 08 Sep 2005 16:09:23 +0200 haftmann introduces some modern-style AList operations
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Mon, 29 Aug 2005 16:18:04 +0200 wenzelm use AList operations;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Fri, 08 Jul 2005 11:57:15 +0200 berghofe Some changes to allow mutually recursive, overloaded functions with same name.
Fri, 01 Jul 2005 14:14:40 +0200 berghofe Adapted to new interface of RecfunCodegen.add.
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, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 21 May 2004 21:15:22 +0200 wenzelm tuned message;
Tue, 18 Nov 2003 09:45:45 +0100 berghofe Improved error handling: add_primrec now prints out ill-formed equation
Thu, 10 Oct 2002 14:26:50 +0200 berghofe Reimplemented parts of datatype package dealing with datatypes involving
Tue, 12 Feb 2002 20:28:27 +0100 wenzelm got rid of explicit marginal comments (now stripped earlier from input);
Wed, 12 Dec 2001 11:07:42 +0100 berghofe Improved error messages.
Mon, 10 Dec 2001 15:34:15 +0100 berghofe Recursive equations to be used for code generation are now registered
Wed, 28 Nov 2001 00:46:26 +0100 wenzelm theory data: removed obsolete finish method;
Wed, 14 Nov 2001 18:45:38 +0100 wenzelm store original simps for codegen;
Thu, 08 Nov 2001 23:59:37 +0100 wenzelm theory data: finish method;
Thu, 18 Oct 2001 21:27:47 +0200 wenzelm GPLed;
Fri, 31 Aug 2001 18:46:48 +0200 wenzelm tuned headers;
Tue, 28 Nov 2000 01:08:50 +0100 wenzelm RuleCases.save;
Thu, 10 Aug 2000 14:55:21 +0200 berghofe Equations that are added to the simpset now have proper names.
Thu, 13 Jul 2000 23:13:10 +0200 wenzelm adapted PureThy.add_defs_i;
Thu, 25 May 2000 15:14:39 +0200 paulson improved error msgs, listing variable names
Wed, 15 Mar 2000 23:39:45 +0100 berghofe Added new theory data slot for primrec equations.
Mon, 13 Mar 2000 13:20:13 +0100 wenzelm adapted to new PureThy.add_thms etc.;
Thu, 21 Oct 1999 18:45:31 +0200 wenzelm proper handling of axioms / defs;
Tue, 05 Oct 1999 15:32:16 +0200 berghofe Got rid of readtm.
Mon, 20 Sep 1999 12:01:41 +0200 berghofe Fixed bug in add_primrec which caused non-informative error message.
Mon, 02 Aug 1999 17:58:23 +0200 wenzelm tuned outer syntax;
Fri, 16 Jul 1999 13:24:41 +0200 berghofe - Now also supports arbitrarily branching datatypes.
Tue, 25 May 1999 20:24:10 +0200 wenzelm formal comments (still dummy);
Mon, 24 May 1999 21:57:13 +0200 wenzelm outer syntax keyword classification;
Wed, 14 Apr 1999 19:05:28 +0200 wenzelm triple_swap;
Wed, 14 Apr 1999 15:58:01 +0200 wenzelm tuned messages;
Wed, 14 Apr 1999 14:42:53 +0200 wenzelm tuned comments;
Wed, 17 Mar 1999 16:53:46 +0100 wenzelm Theory.sign_of;
less more (0) -60 tip