| Sat, 15 Sep 2012 16:09:53 +0200 | traytel | export rel_mono theorem | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | merged two unfold steps | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | took out one rotate_tac | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | killed spurious rotate_tac; use auto instead of blast | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | moved blast tactic to where it is actually needed | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | fixed bug in "mk_map" for the "fun" case | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | correct generalization to 3 or more mutually recursive datatypes | changeset | files |
| Fri, 14 Sep 2012 22:23:11 +0200 | blanchet | provide more guidance, exploiting our knowledge of the goal | changeset | files |