| Wed, 16 May 2012 19:17:20 +0200 |
kuncar |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
changeset |
files
|
| Wed, 16 May 2012 19:15:45 +0200 |
kuncar |
infrastructure that makes possible to prove that a relation is reflexive
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
get ready for automatic generation of extensionality helpers
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
|
changeset |
files
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
more helpful error message
|
changeset |
files
|
| Tue, 15 May 2012 12:07:16 +0200 |
huffman |
transfer rules for many more list constants
|
changeset |
files
|
| Tue, 15 May 2012 13:06:15 +0200 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Tue, 15 May 2012 13:06:15 +0200 |
blanchet |
repair the Waldmeister endgame only for Waldmeister proofs
|
changeset |
files
|
| Tue, 15 May 2012 13:06:15 +0200 |
blanchet |
fixed Waldmeister commutativity hack
|
changeset |
files
|
| Tue, 15 May 2012 13:06:15 +0200 |
blanchet |
imported patch atp_tuning
|
changeset |
files
|
| Tue, 15 May 2012 11:50:34 +0200 |
huffman |
add transfer rules for nat_rec and funpow
|
changeset |
files
|