| changeset 2611 | 3d101f2f817c |
| parent 2593 | 25dcb2b1329e |
| child 2625 | 478c5648e73f |
| 2610:f5c7375ab465 | 2611:3d101f2f817c |
|---|---|
4 |
4 |
5 (* free names in bar are bound in foo *) |
5 (* free names in bar are bound in foo *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 declare [[STEPS = 100]] |
9 thm finite_sets_supp |
10 |
10 |
11 nominal_datatype foo = |
11 nominal_datatype foo = |
12 Foo0 "name" |
12 Foo0 "name" |
13 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f |
13 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f |
14 and bar = |
14 and bar = |