| changeset 2926 | 37c0d7953cba |
| parent 2925 | b4404b13f775 |
| child 2931 | aaef9dec5e1d |
| 2925:b4404b13f775 | 2926:37c0d7953cba |
|---|---|
1 theory Let |
1 theory Let |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
|
4 |
5 |
5 atom_decl name |
6 atom_decl name |
6 |
7 |
7 nominal_datatype trm = |
8 nominal_datatype trm = |
8 Var "name" |
9 Var "name" |
303 apply (simp_all add: fresh_star_Pair) |
304 apply (simp_all add: fresh_star_Pair) |
304 prefer 6 |
305 prefer 6 |
305 apply (erule alpha_bn_inducts) |
306 apply (erule alpha_bn_inducts) |
306 oops |
307 oops |
307 |
308 |
309 |
|
308 end |
310 end |
309 |
311 |
310 |
312 |
311 |
313 |