equal
deleted
inserted
replaced
29 - strong induction rules |
29 - strong induction rules |
30 |
30 |
31 - check support equations for more bindings per constructor |
31 - check support equations for more bindings per constructor |
32 |
32 |
33 - For binding functions that call other binding functions |
33 - For binding functions that call other binding functions |
34 the following are proved with cheat_tac: |
34 the following are proved with cheat_tac: constr_rsp |
35 bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp |
|
36 |
35 |
37 - store information about defined nominal datatypes, so that |
36 - store information about defined nominal datatypes, so that |
38 it can be used to define new types that depend on these |
37 it can be used to define new types that depend on these |
39 |
38 |
40 - make parser aware of recursive and of different versions of abs |
39 - make parser aware of recursive and of different versions of abs |