| Fri, 20 Apr 2012 22:54:13 +0200 |
huffman |
uniform naming scheme for transfer rules
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:49:40 +0200 |
huffman |
rename 'correspondence' method to 'transfer_prover'
|
file |
diff |
annotate
|
| 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
|