src/HOLCF/fixrec_package.ML
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-07-01 huffman 2005-07-01 remove uses of sign_of
2005-06-23 huffman 2005-06-23 New features: permissive option for fixrec to skip proofs of equations; side conditions for fixrec equations (for definedness); fixpat theorem names apply to entire group of theorems; improved error messages
2005-06-20 wenzelm 2005-06-20 added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;
2005-06-18 huffman 2005-06-18 fixrec shows unsolved subgoals when proofs of rewrites fail
2005-06-17 huffman 2005-06-17 support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
2005-06-15 huffman 2005-06-15 allow theorem attributes on fixpat declarations
2005-06-15 huffman 2005-06-15 fixrec package now handles mutually-recursive definitions
2005-06-14 huffman 2005-06-14 cleaned up and reorganized
2005-06-04 huffman 2005-06-04 implementation of fixrec package