| changeset 2451 | d2e929f51fa9 |
| parent 2450 | 217ef3e4282e |
| child 2452 | 39f8d405d7a2 |
| 2450:217ef3e4282e | 2451:d2e929f51fa9 |
|---|---|
33 thm single_let.fv_bn_eqvt |
33 thm single_let.fv_bn_eqvt |
34 thm single_let.size_eqvt |
34 thm single_let.size_eqvt |
35 thm single_let.supports |
35 thm single_let.supports |
36 thm single_let.fsupp |
36 thm single_let.fsupp |
37 |
37 |
38 |
|
39 |
|
40 instantiation trm and assg :: fs |
|
41 begin |
|
42 |
|
43 instance |
|
44 apply(default) |
|
45 apply(simp_all add: single_let.fsupp) |
|
46 done |
|
47 |
|
48 end |
|
49 |
38 |
50 |
39 |
51 |
40 |
52 |
41 |
53 lemma test: |
42 lemma test: |