| Fri, 05 Mar 2010 14:50:37 -0800 | huffman | introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites' | changeset | files |
| Fri, 05 Mar 2010 14:05:25 -0800 | huffman | add comment | changeset | files |
| Fri, 05 Mar 2010 13:56:04 -0800 | huffman | move take_proofs-related stuff to a new section | changeset | files |
| Fri, 05 Mar 2010 13:55:36 -0800 | huffman | remove dead code | changeset | files |
| Fri, 05 Mar 2010 23:52:09 +0100 | wenzelm | tuned dead code; | changeset | files |
| Fri, 05 Mar 2010 23:51:32 +0100 | wenzelm | use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing; | changeset | files |