| Sun, 19 Jun 2011 18:12:49 +0200 | blanchet | fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies | file | diff | annotate |
| Wed, 15 Jun 2011 14:36:41 +0200 | blanchet | use more appropriate type systems for ATP exporter | file | diff | annotate |
| Tue, 07 Jun 2011 07:04:53 +0200 | blanchet | renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules | file | diff | annotate | base |