equal
deleted
inserted
replaced
37 |
37 |
38 - when there are more than one shallow binder, then alpha |
38 - when there are more than one shallow binder, then alpha |
39 equivalence creates more than one permutation. According |
39 equivalence creates more than one permutation. According |
40 to the paper, this is incorrect. |
40 to the paper, this is incorrect. |
41 |
41 |
42 Example in TestMorePerm. |
42 Example in Classical.thy. |
43 |
43 |
|
44 - check whether weirdo example in TestMorePerm works |
|
45 with shallow binders |
44 |
46 |
45 - nested recursion, like types "trm list" in a constructor |
47 - nested recursion, like types "trm list" in a constructor |
46 |
48 |
47 - define permute_bn automatically and prove properties of it |
49 - define permute_bn automatically and prove properties of it |
48 |
50 |