2045
|
1 |
theory Term8
|
|
2 |
imports "../NewParser"
|
|
3 |
begin
|
|
4 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
(* example 8 *)
|
2045
|
6 |
|
|
7 |
atom_decl name
|
|
8 |
|
2147
|
9 |
ML {* val _ = cheat_alpha_bn_rsp := true *}
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
|
2045
|
11 |
nominal_datatype foo =
|
|
12 |
Foo0 "name"
|
|
13 |
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
|
|
14 |
and bar =
|
|
15 |
Bar0 "name"
|
2097
|
16 |
| Bar1 "name" s::"name" b::"bar" bind_set s in b
|
2045
|
17 |
binder
|
|
18 |
bv
|
|
19 |
where
|
|
20 |
"bv (Bar0 x) = {}"
|
|
21 |
| "bv (Bar1 v x b) = {atom v}"
|
|
22 |
|
2147
|
23 |
thm foo_bar.supp
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
|
2045
|
25 |
end
|
|
26 |
|
|
27 |
|