src/HOLCF/fixrec_package.ML
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Fri, 13 Oct 2006 18:28:51 +0200 berghofe Moved old inductive package to old_inductive_package.ML
Wed, 04 Oct 2006 14:17:38 +0200 haftmann insert replacing ins ins_int ins_string
Wed, 19 Jul 2006 12:11:57 +0200 wenzelm Sign.infer_types: Name.context;
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;
Fri, 02 Jun 2006 20:12:59 +0200 wenzelm removed obsolete ML files;
Tue, 07 Feb 2006 19:56:58 +0100 wenzelm adapted Sign.infer_types;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
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;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Fri, 01 Jul 2005 04:00:23 +0200 huffman remove uses of sign_of
Thu, 23 Jun 2005 21:27:23 +0200 huffman New features:
Mon, 20 Jun 2005 22:14:02 +0200 wenzelm added add_fixrec_i, add_fixpat_i;
Sat, 18 Jun 2005 00:38:18 +0200 huffman fixrec shows unsolved subgoals when proofs of rewrites fail
Fri, 17 Jun 2005 21:19:31 +0200 huffman support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
Wed, 15 Jun 2005 21:48:35 +0200 huffman allow theorem attributes on fixpat declarations
Wed, 15 Jun 2005 20:50:38 +0200 huffman fixrec package now handles mutually-recursive definitions
Tue, 14 Jun 2005 04:04:09 +0200 huffman cleaned up and reorganized
Sat, 04 Jun 2005 02:10:19 +0200 huffman implementation of fixrec package
less more (0) tip