| Fri, 17 Apr 2015 16:59:43 +0200 | noschinl | rewrite: work purely conversion-based | file | diff | annotate |
| Fri, 17 Apr 2015 10:49:57 +0200 | noschinl | rewrite: add default pattern "in concl" for more cases | file | diff | annotate |
| Thu, 16 Apr 2015 15:55:55 +0200 | noschinl | rewrite: use distinct names for unnamed abstractions | file | diff | annotate |
| Wed, 15 Apr 2015 15:10:01 +0200 | noschinl | rewrite: add ML interface | file | diff | annotate |
| Mon, 13 Apr 2015 20:11:12 +0200 | noschinl | rewrite: with asm pattern, propagate also remaining assumptions to new subgoals | file | diff | annotate |
| Mon, 13 Apr 2015 15:32:32 +0200 | noschinl | rewrite: do not descend into conclusion of premise with asm pattern | file | diff | annotate |
| Mon, 13 Apr 2015 14:52:40 +0200 | noschinl | rewrite: with asm pattern, try all premises for rewriting, not only the first | file | diff | annotate |