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 ML {* val _ = cheat_alpha_bn_rsp := true *} |
|
10 |
|
11 nominal_datatype foo = |
9 nominal_datatype foo = |
12 Foo0 "name" |
10 Foo0 "name" |
13 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f |
11 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f |
14 and bar = |
12 and bar = |
15 Bar0 "name" |
13 Bar0 "name" |
16 | Bar1 "name" s::"name" b::"bar" bind_set s in b |
14 | Bar1 "name" s::"name" b::"bar" bind (set) s in b |
17 binder |
15 binder |
18 bv |
16 bv |
19 where |
17 where |
20 "bv (Bar0 x) = {}" |
18 "bv (Bar0 x) = {}" |
21 | "bv (Bar1 v x b) = {atom v}" |
19 | "bv (Bar1 v x b) = {atom v}" |
22 |
20 |
|
21 (* |
23 thm foo_bar.supp |
22 thm foo_bar.supp |
|
23 *) |
24 |
24 |
25 end |
25 end |
26 |
26 |
27 |
27 |