equal
deleted
inserted
replaced
4 |
4 |
5 (* example 8 *) |
5 (* example 8 *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* this should work but gives an error at the moment: |
9 ML {* val _ = cheat_alpha_bn_rsp := true *} |
10 in alpha_bn_rsp proof. |
|
11 *) |
|
12 |
10 |
13 nominal_datatype foo = |
11 nominal_datatype foo = |
14 Foo0 "name" |
12 Foo0 "name" |
15 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
13 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
16 and bar = |
14 and bar = |
20 bv |
18 bv |
21 where |
19 where |
22 "bv (Bar0 x) = {}" |
20 "bv (Bar0 x) = {}" |
23 | "bv (Bar1 v x b) = {atom v}" |
21 | "bv (Bar1 v x b) = {atom v}" |
24 |
22 |
|
23 thm foo_bar.supp |
25 |
24 |
26 end |
25 end |
27 |
26 |
28 |
27 |