| Thu, 17 Nov 2011 07:31:37 +0100 | huffman | name simp theorems st_0 and st_1 | changeset | files |
| Thu, 17 Nov 2011 07:15:30 +0100 | huffman | remove redundant simp rules plus_enat_0 | changeset | files |
| Thu, 17 Nov 2011 21:58:10 +0100 | wenzelm | eliminated slightly odd Rep' with dynamically-scoped [simplified]; | changeset | files |
| Thu, 17 Nov 2011 21:31:29 +0100 | wenzelm | partial evaluation in invisible context; | changeset | files |
| Thu, 17 Nov 2011 19:01:05 +0100 | bulwahn | adding a preliminary example to show how the quotient_definition package can be generalized | changeset | files |
| Thu, 17 Nov 2011 18:44:56 +0100 | bulwahn | tuned header | changeset | files |
| Thu, 17 Nov 2011 14:35:32 +0100 | bulwahn | adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition | changeset | files |