2005-06-23 huffman 2005-06-23 added match functions for spair, sinl, sinr
2005-06-18 huffman 2005-06-18 fixrec shows unsolved subgoals when proofs of rewrites fail
2005-06-17 huffman 2005-06-17 added match functions for ONE, TT, and FF; added theorem mplus_fail2
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-15 huffman 2005-06-15 fixrec package now handles mutually-recursive definitions
2005-06-04 huffman 2005-06-04 use fixrec_package.ML
2005-06-04 huffman 2005-06-04 New theory with lemmas for the fixrec package