| Sat, 15 Sep 2012 23:53:10 +0200 | blanchet | tuning | changeset | files |
| Sat, 15 Sep 2012 21:10:26 +0200 | blanchet | tuned code to avoid special case for "fun" | changeset | files |
| Sat, 15 Sep 2012 21:10:26 +0200 | blanchet | tuned induction tactic | changeset | files |
| Sat, 15 Sep 2012 21:10:26 +0200 | blanchet | tuned error message | changeset | files |
| Sat, 15 Sep 2012 21:10:26 +0200 | blanchet | tuning | changeset | files |
| Sat, 15 Sep 2012 20:14:29 +0200 | haftmann | typeclass formalising bounded subtraction | changeset | files |
| Sat, 15 Sep 2012 20:13:25 +0200 | haftmann | dropped some unused identifiers | changeset | files |
| 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 |