| 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
|
| 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
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
fixed issue with bound variables in prem prems + tuning
|
changeset |
files
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
use right version of "mk_UnIN"
|
changeset |
files
|
| Fri, 14 Sep 2012 22:23:10 +0200 |
blanchet |
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
|
changeset |
files
|