| 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 | changeset | files |
| Fri, 17 Jun 2005 18:50:40 +0200 | huffman | added match functions for ONE, TT, and FF; added theorem mplus_fail2 | changeset | files |
| Fri, 17 Jun 2005 18:36:25 +0200 | wenzelm | updated; | changeset | files |
| Fri, 17 Jun 2005 18:35:27 +0200 | wenzelm | accomodate change of TheoryDataFun; | changeset | files |
| Fri, 17 Jun 2005 18:33:42 +0200 | wenzelm | Context.names_of; | changeset | files |
| Fri, 17 Jun 2005 18:33:41 +0200 | wenzelm | * Pure/TheoryDataFun: change of the argument structure; | changeset | files |
| Fri, 17 Jun 2005 18:33:40 +0200 | wenzelm | Sign.root_path, Sign.local_path; | changeset | files |
| Fri, 17 Jun 2005 18:33:39 +0200 | wenzelm | removed obsolete theory_of_sign, theory_of_thm; | changeset | files |