equal
deleted
inserted
replaced
1 theory Term8 |
1 theory Term8 |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example 8 from Terms.thy *) |
5 (* example 8 *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
|
8 |
|
9 (* this should work but gives an error at the moment: |
|
10 seems like in the symmetry proof |
|
11 *) |
8 |
12 |
9 nominal_datatype foo = |
13 nominal_datatype foo = |
10 Foo0 "name" |
14 Foo0 "name" |
11 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
15 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
12 and bar = |
16 and bar = |
13 Bar0 "name" |
17 Bar0 "name" |
14 | Bar1 "name" s::"name" b::"bar" bind_set s in b |
18 | Bar1 "name" s::"name" b::"bar" bind s in b |
15 binder |
19 binder |
16 bv |
20 bv |
17 where |
21 where |
18 "bv (Bar0 x) = {}" |
22 "bv (Bar0 x) = {}" |
19 | "bv (Bar1 v x b) = {atom v}" |
23 | "bv (Bar1 v x b) = {atom v}" |
20 |
24 |
|
25 |
21 end |
26 end |
22 |
27 |
23 |
28 |