| Thu, 05 Apr 2012 16:25:59 +0200 | huffman | use standard quotient lemmas to generate transfer rules | changeset | files | 
| Thu, 05 Apr 2012 15:59:25 +0200 | huffman | add transfer lemmas for quotients | changeset | files | 
| Thu, 05 Apr 2012 15:23:26 +0200 | huffman | define reflp directly, in the manner of symp and transp | changeset | files |