| Fri, 20 Apr 2012 15:49:45 +0200 | huffman | add secondary transfer rule for universal quantifiers on non-bi-total relations | file | diff | annotate |
| Fri, 20 Apr 2012 15:30:13 +0200 | huffman | add transfer rule for 'id' | file | diff | annotate |
| Fri, 20 Apr 2012 10:18:08 +0200 | huffman | make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules | file | diff | annotate |
| Thu, 19 Apr 2012 19:36:09 +0200 | huffman | add transfer rule for Let | file | diff | annotate |
| Tue, 17 Apr 2012 14:00:09 +0200 | huffman | make transfer method more deterministic by using SOLVED' on some subgoals | file | diff | annotate |
| Tue, 17 Apr 2012 11:03:08 +0200 | huffman | add theory data for relator identity rules; | file | diff | annotate |
| Wed, 04 Apr 2012 16:03:01 +0200 | huffman | add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer | file | diff | annotate |
| Tue, 03 Apr 2012 22:31:00 +0200 | huffman | new transfer proof method | file | diff | annotate |